[subversion-commit] SVN tetex-base commit + diffs: r1736 -
tetex-base/trunk/doc/latex/beamer/examples
tetex-doc-nonfree/trunk/doc/latex/beamer/examples
Frank Küster
frank at costa.debian.org
Mon Oct 9 15:18:28 UTC 2006
Author: frank
Date: 2006-10-09 15:18:27 +0000 (Mon, 09 Oct 2006)
New Revision: 1736
Added:
tetex-doc-nonfree/trunk/doc/latex/beamer/examples/beamerexample5.tex
Removed:
tetex-base/trunk/doc/latex/beamer/examples/beamerexample5.tex
Log:
moving contrib beamerexamples files to tetex-doc-nonfree
Deleted: tetex-base/trunk/doc/latex/beamer/examples/beamerexample5.tex
===================================================================
--- tetex-base/trunk/doc/latex/beamer/examples/beamerexample5.tex 2006-10-09 15:18:15 UTC (rev 1735)
+++ tetex-base/trunk/doc/latex/beamer/examples/beamerexample5.tex 2006-10-09 15:18:27 UTC (rev 1736)
@@ -1,1021 +0,0 @@
-% $Header: /cvsroot/latex-beamer/latex-beamer/examples/beamerexample5.tex,v 1.22 2004/10/08 14:02:33 tantau Exp $
-
-\documentclass[11pt]{beamer}
-
-\usetheme{Darmstadt}
-
-\usepackage{times}
-\usefonttheme{structurebold}
-
-\usepackage[english]{babel}
-\usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps}
-\usepackage{amsmath,amssymb}
-\usepackage[latin1]{inputenc}
-
-\setbeamercovered{dynamic}
-
-\newcommand{\Lang}[1]{\operatorname{\text{\textsc{#1}}}}
-
-\newcommand{\Class}[1]{\operatorname{\mathchoice
- {\text{\sf \small #1}}
- {\text{\sf \small #1}}
- {\text{\sf #1}}
- {\text{\sf #1}}}}
-
-\newcommand{\NumSAT} {\text{\small\#SAT}}
-\newcommand{\NumA} {\#_{\!A}}
-
-\newcommand{\barA} {\,\bar{\!A}}
-
-\newcommand{\Nat}{\mathbb{N}}
-\newcommand{\Set}[1]{\{#1\}}
-
-\pgfdeclaremask{tu}{beamer-tu-logo-mask}
-\pgfdeclaremask{computer}{beamer-computer-mask}
-\pgfdeclareimage[interpolate=true,mask=computer,height=2cm]{computerimage}{beamer-computer}
-\pgfdeclareimage[interpolate=true,mask=computer,height=2cm]{computerworkingimage}{beamer-computerred}
-\pgfdeclareimage[mask=tu,height=.5cm]{logo}{beamer-tu-logo}
-
-\logo{\pgfuseimage{logo}}
-
-\title{Weak Cardinality Theorems for First-Order Logic}
-\author{Till Tantau}
-\institute[Technische Universit\"at Berlin]{%
- Fakultät für Elektrotechnik und Informatik\\
- Technische Universit\"at Berlin}
-\date{Fundamentals of Computation Theory 2003}
-
-\colorlet{redshaded}{red!25!bg}
-\colorlet{shaded}{black!25!bg}
-\colorlet{shadedshaded}{black!10!bg}
-\colorlet{blackshaded}{black!40!bg}
-
-\colorlet{darkred}{red!80!black}
-\colorlet{darkblue}{blue!80!black}
-\colorlet{darkgreen}{green!80!black}
-
-\def\radius{0.96cm}
-\def\innerradius{0.85cm}
-
-\def\softness{0.4}
-\definecolor{softred}{rgb}{1,\softness,\softness}
-\definecolor{softgreen}{rgb}{\softness,1,\softness}
-\definecolor{softblue}{rgb}{\softness,\softness,1}
-
-\definecolor{softrg}{rgb}{1,1,\softness}
-\definecolor{softrb}{rgb}{1,\softness,1}
-\definecolor{softgb}{rgb}{\softness,1,1}
-
-\newcommand{\Bandshaded}[2]{
- \color{shadedshaded}
- \pgfmoveto{\pgfxy(-0.5,0)}
- \pgflineto{\pgfxy(-0.6,0.1)}
- \pgflineto{\pgfxy(-0.4,0.2)}
- \pgflineto{\pgfxy(-0.6,0.3)}
- \pgflineto{\pgfxy(-0.4,0.4)}
- \pgflineto{\pgfxy(-0.5,0.5)}
- \pgflineto{\pgfxy(4,0.5)}
- \pgflineto{\pgfxy(4.1,0.4)}
- \pgflineto{\pgfxy(3.9,0.3)}
- \pgflineto{\pgfxy(4.1,0.2)}
- \pgflineto{\pgfxy(3.9,0.1)}
- \pgflineto{\pgfxy(4,0)}
- \pgfclosepath
- \pgffill
-
- \color{black}
- \pgfputat{\pgfxy(0,0.7)}{\pgfbox[left,base]{#1}}
- \pgfputat{\pgfxy(0,-0.1)}{\pgfbox[left,top]{#2}}
-}
-
-\newcommand{\Band}[2]{
- \color{shaded}
- \pgfmoveto{\pgfxy(-0.5,0)}
- \pgflineto{\pgfxy(-0.6,0.1)}
- \pgflineto{\pgfxy(-0.4,0.2)}
- \pgflineto{\pgfxy(-0.6,0.3)}
- \pgflineto{\pgfxy(-0.4,0.4)}
- \pgflineto{\pgfxy(-0.5,0.5)}
- \pgflineto{\pgfxy(4,0.5)}
- \pgflineto{\pgfxy(4.1,0.4)}
- \pgflineto{\pgfxy(3.9,0.3)}
- \pgflineto{\pgfxy(4.1,0.2)}
- \pgflineto{\pgfxy(3.9,0.1)}
- \pgflineto{\pgfxy(4,0)}
- \pgfclosepath
- \pgffill
-
- \color{black}
- \pgfputat{\pgfxy(0,0.7)}{\pgfbox[left,base]{#1}}
- \pgfputat{\pgfxy(0,-0.1)}{\pgfbox[left,top]{#2}}
-}
-
-\newcommand{\BaenderNormal}
-{%
- \pgfsetlinewidth{0.4pt}
- \color{black}
- \pgfputat{\pgfxy(0,5)}{\Band{input tapes}{}}
- \pgfputat{\pgfxy(0.35,4.6)}{\pgfbox[center,base]{$\vdots$}}
- \pgfputat{\pgfxy(0,4)}{\Band{}{}}
-
- \pgfxyline(0,5)(0,5.5)
- \pgfxyline(1.2,5)(1.2,5.5)
- \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$w_1$}}
-
- \pgfxyline(0,4)(0,4.5)
- \pgfxyline(1.8,4)(1.8,4.5)
- \pgfputat{\pgfxy(0.25,4.25)}{\pgfbox[left,center]{$w_n$}}
- \ignorespaces}
-
-\newcommand{\BaenderZweiNormal}
-{%
- \pgfsetlinewidth{0.4pt}
- \color{black}
- \pgfputat{\pgfxy(0,5)}{\Band{Zwei Eingabebänder}{}}
- \pgfputat{\pgfxy(0,4.25)}{\Band{}{}}
-
- \pgfxyline(0,5)(0,5.5)
- \pgfxyline(1.2,5)(1.2,5.5)
- \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$u$}}
-
- \pgfxyline(0,4.25)(0,4.75)
- \pgfxyline(1.8,4.25)(1.8,4.75)
- \pgfputat{\pgfxy(0.25,4.5)}{\pgfbox[left,center]{$v$}}
- \ignorespaces}
-
-\newcommand{\BaenderHell}
-{%
- \pgfsetlinewidth{0.4pt}
- \color{black}
- \pgfputat{\pgfxy(0,5)}{\Bandshaded{input tapes}{}}
- \color{shaded}
- \pgfputat{\pgfxy(0.35,4.6)}{\pgfbox[center,base]{$\vdots$}}
- \pgfputat{\pgfxy(0,4)}{\Bandshaded{}{}}
-
- \color{blackshaded}
- \pgfxyline(0,5)(0,5.5)
- \pgfxyline(1.2,5)(1.2,5.5)
- \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$w_1$}}
-
- \pgfxyline(0,4)(0,4.5)
- \pgfxyline(1.8,4)(1.8,4.5)
- \pgfputat{\pgfxy(0.25,4.25)}{\pgfbox[left,center]{$w_n$}}
- \ignorespaces}
-
-\newcommand{\BaenderZweiHell}
-{%
- \pgfsetlinewidth{0.4pt}
- \color{black}
- \pgfputat{\pgfxy(0,5)}{\Bandshaded{Zwei Eingabebänder}{}}%
- \color{blackshaded}
- \pgfputat{\pgfxy(0,4.25)}{\Bandshaded{}{}}
- \pgfputat{\pgfxy(0.25,4.5)}{\pgfbox[left,center]{$v$}}
- \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$u$}}%
-
- \pgfxyline(0,5)(0,5.5)
- \pgfxyline(1.2,5)(1.2,5.5)
-
- \pgfxyline(0,4.25)(0,4.75)
- \pgfxyline(1.8,4.25)(1.8,4.75)
- \ignorespaces}
-
-\newcommand{\Slot}[1]{%
- \begin{pgftranslate}{\pgfpoint{#1}{0pt}}%
- \pgfsetlinewidth{0.6pt}%
- \color{structure}%
- \pgfmoveto{\pgfxy(-0.1,5.5)}%
- \pgfbezier{\pgfxy(-0.1,5.55)}{\pgfxy(-0.05,5.6)}{\pgfxy(0,5.6)}%
- \pgfbezier{\pgfxy(0.05,5.6)}{\pgfxy(0.1,5.55)}{\pgfxy(0.1,5.5)}%
- \pgflineto{\pgfxy(0.1,4.0)}%
- \pgfbezier{\pgfxy(0.1,3.95)}{\pgfxy(0.05,3.9)}{\pgfxy(0,3.9)}%
- \pgfbezier{\pgfxy(-0.05,3.9)}{\pgfxy(-0.1,3.95)}{\pgfxy(-0.1,4.0)}%
- \pgfclosepath%
- \pgfstroke%
- \end{pgftranslate}\ignorespaces}
-
-\newcommand{\SlotZwei}[1]{%
- \begin{pgftranslate}{\pgfpoint{#1}{0pt}}%
- \pgfsetlinewidth{0.6pt}%
- \color{structure}%
- \pgfmoveto{\pgfxy(-0.1,5.5)}%
- \pgfbezier{\pgfxy(-0.1,5.55)}{\pgfxy(-0.05,5.6)}{\pgfxy(0,5.6)}%
- \pgfbezier{\pgfxy(0.05,5.6)}{\pgfxy(0.1,5.55)}{\pgfxy(0.1,5.5)}%
- \pgflineto{\pgfxy(0.1,4.25)}%
- \pgfbezier{\pgfxy(0.1,4.25)}{\pgfxy(0.05,4.15)}{\pgfxy(0,4.15)}%
- \pgfbezier{\pgfxy(-0.05,4.15)}{\pgfxy(-0.1,4.2)}{\pgfxy(-0.1,4.25)}%
- \pgfclosepath%
- \pgfstroke%
- \end{pgftranslate}\ignorespaces}
-
-\newcommand{\ClipSlot}[1]{%
- \pgfrect[clip]{\pgfrelative{\pgfxy(-0.1,0)}{\pgfpoint{#1}{4cm}}}{\pgfxy(0.2,1.5)}\ignorespaces}
-
-\newcommand{\ClipSlotZwei}[1]{%
- \pgfrect[clip]{\pgfrelative{\pgfxy(-0.1,0)}{\pgfpoint{#1}{4.25cm}}}{\pgfxy(0.2,1.25)}\ignorespaces}
-
-
-\AtBeginSection[]{\frame{\frametitle{Outline}\tableofcontents[current]}}
-
-\begin{document}
-
-\frame{\titlepage}
-
-%\section*{Outline}
-\part{Main Part}
-\frame{\frametitle{Outline}\tableofcontents[part=1]}
-
-\section{History}
-
-\subsection{Enumerability in Recursion and Automata Theory}
-
-\frame
-{
- \frametitle{Motivation of Enumerability}
-
- \begin{block}{Problem}
- Many functions are not computable or not efficiently computable.
- \end{block}
- \vskip-1em
- \begin{overprint}
- \onslide<1-2>
- \begin{example}
- \begin{overprint}
- \onslide<1>
- \vskip0.5em
- \begin{itemize}
- \item
- $\NumSAT$:\\
- How many satisfying assignments does a formula have?
- \end{itemize}
-
- \onslide<2>
- \vskip0.5em
- For difficult languages~$A$:
- \begin{itemize}
- \item
- Cardinality function $\NumA^n$:\\
- \alert{How many} input words are in~$A$?
- \item
- Characteristic function $\chi_A^n$:\\
- \alert{Which} input words are in~$A$?
- \end{itemize}
- \begin{pgfpicture}{-9cm}{0.75cm}{-9cm}{2cm}
-
- \pgfnodebox{words}[virtual]{\pgfxy(0,3.5)}{$(w_1, \alert{w_2},
- w_3, w_4, \alert{w_5})$}{2pt}{5pt}
-
- \color{red}
- \pgfputat{\pgfxy(0.75,4.5)}{\pgfbox[center,base]{in $A$}}
- \pgfxyline(0.75,4.4)(-0.6,3.7)
- \pgfxyline(0.75,4.4)(1.2,3.7)
- \color{black}
-
- \pgfnodebox{number}[virtual]{\pgfxy(-1,1)}{2}{2pt}{2pt}
- \pgfnodebox{string}[virtual]{\pgfxy(1,1)}{0\alert{1}00\alert{1}}{2pt}{2pt}
-
- \pgfsetstartarrow{\pgfarrowbar}
- \pgfsetendarrow{\pgfarrowto}
-
- \pgfnodeconnline{words}{string}%{-60}{120}{1cm}{1cm}
- \pgfnodeconnline{words}{number}%{-120}{60}{1cm}{1cm}
-
- \pgfputat{\pgfxy(-0.9,2.3)}{\pgfbox[center,base]{$\NumA^5$}}
- \pgfputat{\pgfxy(0.9,2.3)}{\pgfbox[center,base]{$\chi_A^5$}}
- \end{pgfpicture}
- \end{overprint}
- \end{example}
-
- \onslide<3>
- \begin{block}{Solutions}
- Difficult functions can be
- \begin{itemize}
- \item
- computed using probabilistic algorithms,
- \item
- computed efficiently on average,
- \item
- approximated, or
- \item<alert at 1->
- enumerated.
- \end{itemize}
- \end{block}
- \end{overprint}
-}
-
-\frame
-{
- \frametitle{Enumerators Output Sets of Possible Function Values}
- \begin{columns}
- \begin{column}{4.5cm}
- \begin{pgfpicture}{-0.5cm}{0cm}{4cm}{6cm}
-
- \pgfputat{\pgfxy(0,0.5)}{\Band{}{output tape}}
-
- \BaenderHell
-
- \color{black}
-
- \only<1-4,6->{\pgfputat{\pgfxy(1.75,2.5)}{\pgfbox[center,center]{\pgfuseimage{computerimage}}}}
- \only<5>{\pgfputat{\pgfxy(1.75,2.5)}{\pgfbox[center,center]{\pgfuseimage{computerworkingimage}}}}
-
- \begin{pgfscope}
- \only<1>{\ClipSlot{0cm}}
- \only<2>{\ClipSlot{0.6cm}}
- \only<3>{\ClipSlot{1.2cm}}
- \only<4->{\ClipSlot{1.8cm}}
- \BaenderNormal
- \end{pgfscope}
-
- \only<1>{\Slot{0cm}}
- \only<2>{\Slot{0.6cm}}
- \only<3>{\Slot{1.2cm}}
- \only<4->{\Slot{1.8cm}}
-
- \only<6->{
- \pgfxyline(0,0.5)(0,1)
- \pgfxyline(1,0.5)(1,1)
- \pgfputat{\pgfxy(0.5,0.75)}{\pgfbox[center,center]{$u_1$}}}
- \only<7->{
- \pgfxyline(2,0.5)(2,1)
- \pgfputat{\pgfxy(1.5,0.75)}{\pgfbox[center,center]{\alert<9>{$u_2$}}}}
- \only<8->{
- \pgfxyline(3,0.5)(3,1)
- \pgfputat{\pgfxy(2.5,0.75)}{\pgfbox[center,center]{$u_3$}}}
-
- \pgfsetlinewidth{0.6pt}
- \color{structure}
- \pgfsetendarrow{\pgfarrowto}
-
- \pgfsetlinewidth{0.6pt}
- \color{structure}
- \pgfsetendarrow{\pgfarrowto}
- \only<-5>{\pgfxycurve(1.75,1.5)(1.75,1)(0,1.5)(0,1.05)}
- \only<6>{\pgfxycurve(1.75,1.5)(1.75,1)(1,1.5)(1,1.05)}
- \only<7>{\pgfxycurve(1.75,1.5)(1.75,1)(2,1.5)(2,1.05)}
- \only<8->{\pgfxycurve(1.75,1.5)(1.75,1)(3,1.5)(3,1.05)}
-
- \only<1>{\pgfxycurve(1.75,3.5)(1.75,3.75)(0,3.5)(0,3.85)}
- \only<2>{\pgfxycurve(1.75,3.5)(1.75,3.75)(0.6,3.5)(0.6,3.85)}
- \only<3>{\pgfxycurve(1.75,3.5)(1.75,3.75)(1.2,3.5)(1.2,3.85)}
- \only<4->{\pgfxycurve(1.75,3.5)(1.75,3.75)(1.8,3.5)(1.8,3.85)}
- \end{pgfpicture}
- \end{column}
- \begin{column}{6.5cm}
- \begin{definition}[1987, 1989, 1994, 2001]
- An \alert{$m$-enumerator} for a function~$f$
- \begin{enumerate}
- \item<alert at 1-4>
- reads $n$ input words $w_1$, \dots, $w_n$,
- \item<alert at 5>
- does a computation,
- \item<alert at 6-8>
- outputs at most $m$ values,
- \item<alert at 9>
- one of which is $f(w_1,\dots,w_n)$.
- \end{enumerate}
- \end{definition}
- \end{column}
- \end{columns}
-}
-
-\subsection{Known Weak Cardinality Theorem}
-
-\frame
-{
- \frametitle{How Well Can the Cardinality Function Be Enumerated?}
-
- \begin{block}{Observation}
- For fixed~$n$, the cardinality function $\NumA^n$
- \begin{itemize}
- \item
- can be \alert{$1$}-enumerated by Turing machines only for \alert{recursive}~$A$,~but\hskip-0.5cm\hbox{}
- \item
- can be \alert{$(n+1)$}-enumerated for \alert{every} language~$A$.
- \end{itemize}
- \end{block}
-
- \begin{alertblock}{Question}<2->
- What about $2$-, $3$-, $4$-, \dots, $n$-enumerability?
- \end{alertblock}
-}
-
-\newtheorem{card}{Cardinality Theorem}[theorem]
-\newtheorem{weakcard}{Weak Cardinality Theorems}[theorem]
-
-\frame
-{
- \frametitle{How Well Can the Cardinality Function\\ Be Enumerated
- by Turing Machines?}
-
- \begin{card}[Kummer, 1992]
- If $\NumA^n$ is $n$-enumerable by a Turing machine, then $A$ is
- recursive.
- \end{card}
-
- \begin{weakcard}[\uncover<2->{\alert<1-2>{1987},} \uncover<3->{\alert<3>{1989},}
- \uncover<4->{\alert<4>{1992}}]<2->
- \begin{enumerate}
- \item<2-| alert at 2>
- If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$ is
- recursive.
- \item<3-| alert at 3>
- If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$ is
- recursive.
- \item<4-| alert at 4>
- If $\NumA^n$ is $n$-enumerable by a Turing machine that never
- enumerates both $0$ and~$n$, then $A$ is recursive.
- \end{enumerate}
- \end{weakcard}
-}
-
-
-\frame
-{
- \frametitle{How Well Can the Cardinality Function\\ Be Enumerated
- by Finite Automata?}
-
- \begin{alertblock}{Conjecture}
- If $\NumA^n$ is $n$-enumerable by a \alert{finite automaton}, then $A$ is
- \alert{regular}.
- \end{alertblock}
-
- \begin{weakcard}[2001, 2002]
- \begin{enumerate}
- \item
- If $\chi_A^n$ is $n$-enumerable by a \alert{finite automaton}, then $A$ is
- \alert{regular}.
- \item
- If $\NumA^2$ is $2$-enumerable by a \alert{finite automaton}, then $A$ is
- \alert{regular}.
- \item
- If $\NumA^n$ is $n$-enumerable by a \alert{finite automaton} that never
- enumerates both $0$ and~$n$, then $A$ is \alert{regular}.
- \end{enumerate}
- \end{weakcard}
-}
-
-
-\subsection{Why Do Cardinality Theorems Hold Only for Certain Models?}
-
-\frame
-{
- \frametitle{Cardinality Theorems Do Not Hold for All Models}
-
- \begin{pgfpicture}{-2.5cm}{0.3cm}{0.5cm}{6.5cm}
- \pgfsetlinewidth{0.6pt}
-
- \pgfsetendarrow{\pgfarrowto}
- \pgfxyline(0,0.5)(0,6.5)
- \pgfclearendarrow
-
- \pgfputat{\pgfxy(-0.2,5.75)}{\pgfbox[right,base]{Turing machines}}
-
- \only<2>{
- \pgfputat{\pgfxy(-0.2,3.75)}{\pgfbox[right,base]{\alert{resource-bounded}}}
- \pgfputat{\pgfxy(-0.2,3.25)}{\pgfbox[right,base]{\alert{machines}}}
- \pgfcircle[fill]{\pgfxy(0,3.6)}{2pt}
- \pgfputat{\pgfxy(0.4,3.5)}{\pgfbox[left,base]{Weak cardinality
- theorems do \alert{not} hold.}}}
-
- \pgfputat{\pgfxy(-0.2,1.5)}{\pgfbox[right,base]{finite}}
- \pgfputat{\pgfxy(-0.2,1)}{\pgfbox[right,base]{automata}}
-
- \pgfcircle[fill]{\pgfxy(0,5.85)}{2pt}
- \pgfcircle[fill]{\pgfxy(0,1.35)}{2pt}
-
- \pgfputat{\pgfxy(0.4,5.75)}{\pgfbox[left,base]{Weak cardinality
- theorems hold.}}
- \pgfputat{\pgfxy(0.4,1.25)}{\pgfbox[left,base]{Weak cardinality
- theorems hold.}}
- \end{pgfpicture}
-}
-
-\frame
-{
- \frametitle{Why?}
-
- \begin{block}{First Explanation}<1>
- The weak cardinality theorems hold both for recursion and automata
- theory \alert{by coincidence}.
- \end{block}
-
- \begin{block}{Second Explanation}<1-2>
- The weak cardinality theorems hold both for
- recursion and automata theory, \alert{because they are
- instantiations of\\ single, unifying theorems}.
- \end{block}
-
- \vskip1em
- \visible<2->{
- The second explanation is correct.\\
- The theorems can (almost) be unified using first-order logic.
- }
-}
-
-
-
-\section[Unification by Logic]{Unification by First-Order Logic}
-
-\subsection{Elementary Definitions}
-
-\frame
-{
- \frametitle{What Are Elementary Definitions?}
-
- \begin{definition}
- A relation~$R$ is \alert{elementarily definable in a
- logical structure~$\mathcal S$} if
- \begin{enumerate}
- \item
- there exists a first-order formula~$\phi$,
- \item
- that is true exactly for the elements of~$R$.
- \end{enumerate}
- \end{definition}
-
- \begin{example}
- The set of even numbers is elementarily definable in $(\Nat, +)$
- via the formula $\phi(x) \equiv \exists z \centerdot z+z=x$.
- \end{example}
-
- \begin{example}
- The set of powers of 2 is not elementarily definable in $(\Nat, +)$.
- \end{example}
-}
-
-
-\frame
-{
- \frametitle{Characterisation of Classes by Elementary Definitions}
-
- \begin{theorem}[B\"uchi, 1960]
- There exists a logical structure~$(\Nat, +, \mathrm e_2)$
- such that a set $A \subseteq \Nat$ is\\ \alert{regular} iff it is
- \alert{elementarily definable in~$(\Nat, +, \mathrm e_2)$}.
- \end{theorem}
-
- \begin{theorem}
- There exists a logical structure~$\mathcal R$ such that a set $A
- \subseteq \Nat$ is \alert{recursively enumerable} iff it is \alert{positively
- elementarily definable in~$\mathcal R$}.\hskip-0.5cm\hbox{}
- \end{theorem}
-}
-
-
-
-\frame
-{
- \frametitle{Characterisation of Classes by Elementary Definitions}
-
- \begin{pgfpicture}{-5.4cm}{0.3cm}{5.4cm}{6.5cm}
- \pgfsetlinewidth{0.6pt}
-
- \pgfsetendarrow{\pgfarrowto}
- \pgfxyline(0,0.3)(0,6.5)
- \pgfclearendarrow
-
- \only<2->{
- \pgfputat{\pgfxy(-0.3,0.5)}{\pgfbox[right,base]{Presburger arithmetic}}
- \pgfcircle[fill]{\pgfxy(0,0.6)}{2pt}
- \pgfputat{\pgfxy(0.3,0.5)}{\pgfbox[left,base]{$(\Nat, +)$}}
- }
- \pgfputat{\pgfxy(-0.3,1.5)}{\pgfbox[right,base]{regular sets}}
- \pgfcircle[fill]{\pgfxy(0,1.6)}{2pt}
- \pgfputat{\pgfxy(0.3,1.5)}{\pgfbox[left,base]{$(\Nat, +, \mathrm e_2)$}}
-
- \pgfputat{\pgfxy(-0.3,2.5)}{\pgfbox[right,base]{\alert{resource-bounded classes}}}
- \pgfcircle[fill]{\pgfxy(0,2.6)}{2pt}
- \pgfputat{\pgfxy(0.3,2.5)}{\pgfbox[left,base]{\alert{none}}}
-
- \pgfputat{\pgfxy(-0.3,3.5)}{\pgfbox[right,base]{recursively enumerable sets}}
- \pgfcircle[fill]{\pgfxy(0,3.6)}{2pt}
- \pgfputat{\pgfxy(0.3,3.5)}{\pgfbox[left,base]{positively in $\mathcal R$}}
-
- \only<2->{
- \pgfputat{\pgfxy(-0.3,4.5)}{\pgfbox[right,base]{arithmetic hierarchy}}
- \pgfcircle[fill]{\pgfxy(0,4.6)}{2pt}
- \pgfputat{\pgfxy(0.3,4.5)}{\pgfbox[left,base]{$(\Nat, +, \cdot)$}}
-
- \pgfputat{\pgfxy(-0.3,5.5)}{\pgfbox[right,base]{ordinal number arithmetic}}
- \pgfcircle[fill]{\pgfxy(0,5.6)}{2pt}
- \pgfputat{\pgfxy(0.3,5.5)}{\pgfbox[left,base]{$(\mathrm{On}, +, \cdot)$}}}
- \end{pgfpicture}
-}
-
-
-\subsection{Enumerability for First-Order Logic}
-
-\frame
-{
- \frametitle{Elementary Enumerability is a Generalisation of\\ Elementary Definability}
-
- \begin{columns}
- \begin{column}{3.25cm}
- \begin{pgfpicture}{-0.25cm}{0cm}{3cm}{4cm}
-
- \color{shaded}
- \pgfmoveto{\pgfxy(0,1.3)}
- \pgfcurveto{\pgfxy(0.5,2.3)}{\pgfxy(2,1.5)}{\pgfxy(2.5,2.3)}
- \pgflineto{\pgfxy(2.5,1.7)}
- \pgfcurveto{\pgfxy(2,0.7)}{\pgfxy(1,1.7)}{\pgfxy(0,0.5)}
- \pgfclosepath
- \pgffill
-
- \pgfsetlinewidth{0.8pt}
- \color{black}
- \pgfmoveto{\pgfxy(0,1)}
- \pgflineto{\pgfxy(0.25,1.15)}
- \pgflineto{\pgfxy(0.5,1.5)}
- \pgflineto{\pgfxy(1,1.7)}
- \pgflineto{\pgfxy(1.5,1.5)}
- \pgflineto{\pgfxy(2,1.4)}
- \pgflineto{\pgfxy(2.25,1.5)}
- \pgflineto{\pgfxy(2.5,2)}
- \pgfstroke
-
- \pgfsetlinewidth{0.4pt}
- \pgfsetendarrow{\pgfarrowto}
- \pgfxyline(0,0)(2.5,0)
- \pgfxyline(0,0)(0,3)
- \pgfputat{\pgfxy(0.5,1.9)}{\pgfbox[center,base]{$R$}}
- \pgfputat{\pgfxy(2.6,0)}{\pgfbox[left,center]{$x$}}
- \pgfputat{\pgfxy(0,3.2)}{\pgfbox[center,base]{$f(x)$}}
- \pgfputat{\pgfxy(2.55,2)}{\pgfbox[left,center]{$f$}}
- \end{pgfpicture}
- \end{column}
- \begin{column}{7.5cm}
- \begin{definition}
- A function~$f$ is\\
- \alert{elementarily $m$-enumerable in a structure~$\mathcal S$} if
- \begin{enumerate}
- \item
- its graph is contained in an\\
- \alert{elementarily definable} relation~$R$,
- \item
- which is \alert{$m$-bounded}, i.\kern1pt e., for each~$x$
- there are at most~$m$ different~$y$ with $(x,y) \in R$.
- \end{enumerate}
- \end{definition}
- \end{column}
- \end{columns}
-}
-
-\frame
-{
- \frametitle{The Original Notions of Enumerability are Instantiations}
-
- \begin{theorem}
- A function is $m$-enumerable by a \alert{finite automaton} iff\\
- it is elementarily $m$-enumerable in \alert{$(\Nat, +, \mathrm e_2)$}.
- \end{theorem}
-
- \begin{theorem}
- A function is $m$-enumerable by a \alert{Turing machine} iff\\
- it is positively elementarily $m$-enumerable in \alert{$\mathcal R$}.
- \end{theorem}
-}
-
-%\subsection{Cross Product Theorem for First-Order Logic}
-
-\subsection{Weak Cardinality Theorems for First-Order Logic}
-
-\frame
-{
- \frametitle{The First Weak Cardinality Theorem}
-
- \begin{theorem}
- Let $\mathcal S$ be a logical structure with universe~$U$ and let
- $A \subseteq U$. If
-
- \begin{enumerate}
- \item
- $\mathcal S$ is well-orderable and
- \item
- \alert{$\chi_A^n$} is elementarily \alert{$n$}-enumerable in~$\mathcal S$,
- \end{enumerate}
-
- then \alert{$A$ is elementarily definable} in~$\mathcal S$.
- \end{theorem}
- \begin{overprint}
- \onslide<2>
- \begin{corollary}
- If $\chi_A^n$ is $n$-enumerable by a finite automaton, then
- $A$ is regular.
- \end{corollary}
-
- \onslide<3>
- \begin{corollary}[with more effort]
- If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$
- is recursive.
- \end{corollary}
- \end{overprint}
-}
-
-\frame
-{
- \frametitle{The Second Weak Cardinality Theorem}
-
- \begin{theorem}
- Let $\mathcal S$ be a logical structure with universe~$U$ and let
- $A \subseteq U$. If
-
- \begin{enumerate}
- \item
- $\mathcal S$ is well-orderable,
- \item
- every finite relation on~$U$ is elementarily definable
- in~$\mathcal S$, and
- \item
- \alert{$\NumA^2$} is elementarily \alert{$2$}-enumerable in~$\mathcal S$,
- \end{enumerate}
-
- then \alert{$A$ is elementarily definable} in~$\mathcal S$.
- \end{theorem}
-% \begin{overlayarea}{\textwidth}{2cm}
-% \only<2>{
-% \begin{corollary}
-% If $\NumA^2$ is $2$-enumerable by a finite automaton, then
-% $A$ is regular.
-% \end{corollary}}%
-% \only<3>{
-% \begin{block}{Corollary}
-% If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$
-% is recursive in the halting problem.
-% \end{block}
-% }
-% \end{overlayarea}
-}
-
-\frame
-{
- \frametitle{The Third Weak Cardinality Theorem}
-
- \begin{theorem}
- Let $\mathcal S$ be a logical structure with universe~$U$ and let
- $A \subseteq U$. If
-
- \begin{enumerate}
- \item
- $\mathcal S$ is well-orderable,
- \item
- every finite relation on~$U$ is elementarily definable
- in~$\mathcal S$, and
- \item
- \alert{$\NumA^n$} is elementarily \alert{$n$}-enumerable in~$\mathcal S$ via a
- relation that \alert{never `enumerates' both $0$ and~$n$},
- \end{enumerate}
-
- then \alert{$A$ is elementarily definable} in~$\mathcal S$.
- \end{theorem}
-% \begin{overlayarea}{\textwidth}{2cm}
-% \only<2>{
-% \begin{corollary}
-% If $\NumA^n$ is $n$-enumerable by a finite automaton that
-% never enumerates both $0$ and~$n$, then $A$ is regular.
-% \end{corollary}}%
-% \only<3>{
-% \begin{block}{Corollary}
-% If $\NumA^n$ is $n$-enumerable by a Turing machine that never
-% enumerates both $0$ and~$n$, then $A$ is recursive in the
-% halting problem.
-% \end{block}
-% }
-% \end{overlayarea}
-}
-
-
-
-\frame
-{
- \frametitle{Relationships Between Cardinality Theorems (CT)}
-
- \begin{pgfpicture}{0cm}{0cm}{10cm}{5cm}
- \only<2>{%
- \color{alert}
- \pgfnodebox{autX}[virtual]{\pgfxy(2.2,4)}{CT}{2pt}{2pt}
- \color{black}}%
- \pgfnodebox{autA}[virtual]{\pgfxy(1,3)}{1st Weak CT}{2pt}{2pt}
- \pgfnodebox{autB}[virtual]{\pgfxy(1,2)}{2nd Weak CT}{2pt}{2pt}
- \pgfnodebox{autC}[virtual]{\pgfxy(1,1)}{3rd Weak CT}{2pt}{2pt}
-
- \only<2>{%
- \color{alert}
- \pgfnodebox{logX}[virtual]{\pgfxy(6.2,4.5)}{CT}{2pt}{2pt}%
- \color{black}}%
- \pgfnodebox{logA}[virtual]{\pgfxy(5,3.5)}{1st Weak CT}{2pt}{2pt}
- \pgfnodebox{logB}[virtual]{\pgfxy(5,2.5)}{2nd Weak CT}{2pt}{2pt}
- \pgfnodebox{logC}[virtual]{\pgfxy(5,1.5)}{3rd Weak CT}{2pt}{2pt}
-
- \pgfnodebox{recX}[virtual]{\pgfxy(10.2,4)}{CT}{2pt}{2pt}
- \pgfnodebox{recA}[virtual]{\pgfxy(9,3)}{1st Weak CT}{2pt}{2pt}
- \pgfnodebox{recB}[virtual]{\pgfxy(9,2)}{2nd Weak CT}{2pt}{2pt}
- \pgfnodebox{recC}[virtual]{\pgfxy(9,1)}{3rd Weak CT}{2pt}{2pt}
-
- \pgfputat{\pgfxy(1,4.5)}{\pgfbox[center,base]{\structure{automata theory}}}
- \pgfputat{\pgfxy(5,5)}{\pgfbox[center,base]{\structure{first-order logic}}}
- \pgfputat{\pgfxy(9,4.5)}{\pgfbox[center,base]{\structure{recursion
- theory}}}
-
- {%
- \color{structure}%
- \pgfxyline(3,0)(3,5)
- \pgfxyline(7,0)(7,5)
- }%
- \pgfsetendarrow{\pgfarrowto}
- \pgfnodeconnline{logA}{autA}
- \pgfnodeconnline{logA}{recA}
- \pgfnodeconnline{logB}{autB}
- \pgfnodeconnline{logC}{autC}
-
- \pgfnodeconncurve{recX}{recA}{-60}{5}{10pt}{10pt}
- \pgfnodeconncurve{recX}{recB}{-55}{5}{10pt}{20pt}
- \pgfnodeconncurve{recX}{recC}{-50}{5}{10pt}{30pt}
-
- \only<2>{%
- \alert{
- \pgfnodeconnline{logX}{autX}
- \pgfnodeconncurve{logX}{logA}{-60}{0}{10pt}{10pt}
- \pgfnodeconncurve{logX}{logB}{-55}{0}{10pt}{20pt}
- \pgfnodeconncurve{logX}{logC}{-50}{0}{10pt}{30pt}
- \pgfnodeconncurve{autX}{autA}{-60}{11}{10pt}{10pt}
- \pgfnodeconncurve{autX}{autB}{-55}{11}{10pt}{20pt}
- \pgfnodeconncurve{autX}{autC}{-50}{11}{10pt}{30pt}
- }
- }
-
- \pgfsetdash{{3pt}{3pt}}{0pt}
- \pgfnodeconnline{logB}{recB}
- \pgfnodeconnline{logC}{recC}
-
- \only<2>{%
- \alert{\pgfnodeconnline{logX}{recX}}}
- \end{pgfpicture}
-}
-
-
-\section{Applications}
-
-\subsection{A Separability Result for First-Order Logic}
-
-%\frame
-%{
-% \begin{columns}
-% \begin{column}{2.4cm}
-% \begin{pgfpicture}{-1.2cm}{-1.2cm}{1cm}{1cm}
-% \color{shaded}
-% \pgfrect[fill]{\pgfxy(-1.4,-1)}{\pgfxy(2.8,2)}
-
-% \color{white}
-% \pgfcircle[fill]{\pgfxy(-0.6,0)}{0.5cm}
-% \pgfcircle[fill]{\pgfxy(0.6,0)}{0.5cm}
-% \only<2->{%
-% \color{softred}
-% \pgfcircle[fill]{\pgfxy(-0.6,0)}{0.6cm}}%
-% %
-% \color{black}
-% \pgfcircle[stroke]{\pgfxy(-0.6,0)}{0.5cm}
-% \pgfcircle[stroke]{\pgfxy(0.6,0)}{0.5cm}
-
-% \pgfputat{\pgfxy(-0.6,0)}{\pgfbox[center,center]{$A^{(n)}$}}
-% \pgfputat{\pgfxy(0.6,0)}{\pgfbox[center,center]{$\barA{}^{(n)}$}}
-% \end{pgfpicture}
-% \end{column}
-% \begin{column}{8cm}
-% \begin{block}{Notation}
-% Let $A^{(n)}$ contain all $n$ tuples of\\
-% distinct elements of~$A$.
-% \end{block}
-
-% \begin{block}{Theorem}
-% Let $\mathcal S$ be a well-orderable logical structure in which
-% all finite relations are elementarily definable.\\[0.5em]
-% If $A^{(n)}$ and $\barA{}^{(n)}$ are \alert<2>{elementarily separable}
-% in~$\mathcal S$, then~so~are~$A$~and~$\barA$.
-% \end{block}
-
-% \uncover<3>{
-% \begin{alertblock}{Note}
-% The theorem is no longer true if $\barA$ is replaced by an
-% arbitrary set~$B$.
-% \end{alertblock}
-% }
-% \end{column}
-% \end{columns}
-%}
-
-
-\frame
-{
- \begin{columns}
- \begin{column}{4cm}
- \begin{pgfpicture}{-2cm}{-1.75cm}{2cm}{2.25cm}
- \color{shaded}
- \pgfrect[fill]{\pgfxy(-2,-1.75)}{\pgfxy(4,4)}
- %\pgfcircle[fill]{\pgforigin}{2cm}
-
- \only<1>{%
- \color{white}%
- \pgfcircle[fill]{\pgfpolar{90}{1cm}}{\innerradius}
- \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\innerradius}
- \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\innerradius}}%
- \only<2->{%
- \color{softred}
- \pgfcircle[fill]{\pgfpolar{90}{1cm}}{\radius}
- \color{softgreen}
- \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\radius}
- \color{softblue}
- \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}}%
- %
- \only<2->{%
- \begin{pgftranslate}{\pgfpolar{90}{1cm}}
- \pgfzerocircle{\radius}
- \pgfclip
-
- \begin{pgftranslate}{\pgfpolar{-90}{1cm}}
- \color{softrb}
- \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}
- \color{softrg}
- \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\radius}
- \end{pgftranslate}
- \end{pgftranslate}
-
- \begin{pgftranslate}{\pgfpolar{210}{1cm}}
- \pgfzerocircle{\radius}
- \pgfclip
-
- \begin{pgftranslate}{\pgfpolar{30}{1cm}}
- \color{softgb}
- \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}
- \end{pgftranslate}
- \end{pgftranslate}}%
- %
- \color{black}
- \pgfcircle[stroke]{\pgfpolar{90}{1cm}}{\innerradius}
- \pgfcircle[stroke]{\pgfpolar{210}{1cm}}{\innerradius}
- \pgfcircle[stroke]{\pgfpolar{330}{1cm}}{\innerradius}
-
- \pgfputat{\pgfrelative{\pgfpolar{90}{1cm}}%
- {\pgfpoint{0pt}{-.5ex}}}%
- {\pgfbox[center,base]{$A\times \barA$}}
- \pgfputat{\pgfrelative{\pgfpolar{210}{1cm}}%
- {\pgfpoint{0pt}{-.5ex}}}%
- {\pgfbox[center,base]{$A\times A$}}
- \pgfputat{\pgfrelative{\pgfpolar{330}{1cm}}%
- {\pgfpoint{0pt}{-.5ex}}}%
- {\pgfbox[center,base]{$\barA\times \barA$}}
-
- \end{pgfpicture}
- \end{column}
- \begin{column}{6.8cm}
- \begin{theorem}
- Let $\mathcal S$ be a well-orderable logical structure in which
- all finite relations are elementarily definable.\\[0.5em]
- If there exist elementarily definable supersets of
- {\color<2>{darkgreen}$A \times A$},
- {\color<2>{darkred}$A \times \barA$}, and
- {\color<2>{darkblue}$\barA \times \barA$} whose
- intersection is empty,\\
- then $A$ is elementarily definable in~$\mathcal S$.
- \end{theorem}
- \begin{alertblock}{Note}<3>
- The theorem is no longer true\\
- if we add $\barA \times A$ to the list.
- \end{alertblock}%
- \end{column}
- \end{columns}
-}
-
-
-\section*{Summary}
-
-\frame
-{
- \frametitle{Summary}
-
- \begin{block}{Summary}
- \begin{itemize}
- \item
- The weak cardinality theorems for first-order logic \alert{unify}\\
- the weak cardinality theorems of automata and recursion theory.
- \item
- The logical approach yields
- weak cardinality theorems for\\ \alert{other computational models}.
- \item
- Cardinality theorems are \alert{separability theorems} in disguise.
- \end{itemize}
- \end{block}{}
-
- \begin{block}{Open Problems}
- \begin{itemize}
- \item
- Does a cardinality theorem for first-order logic hold?
- \item
- What about non-well-orderable structures like $(\mathbb R, +,
- \cdot)$?
- \end{itemize}
- \end{block}
-}
-
-\end{document}
-
-
Copied: tetex-doc-nonfree/trunk/doc/latex/beamer/examples/beamerexample5.tex (from rev 1735, tetex-base/trunk/doc/latex/beamer/examples/beamerexample5.tex)
===================================================================
--- tetex-doc-nonfree/trunk/doc/latex/beamer/examples/beamerexample5.tex (rev 0)
+++ tetex-doc-nonfree/trunk/doc/latex/beamer/examples/beamerexample5.tex 2006-10-09 15:18:27 UTC (rev 1736)
@@ -0,0 +1,1021 @@
+% $Header: /cvsroot/latex-beamer/latex-beamer/examples/beamerexample5.tex,v 1.22 2004/10/08 14:02:33 tantau Exp $
+
+\documentclass[11pt]{beamer}
+
+\usetheme{Darmstadt}
+
+\usepackage{times}
+\usefonttheme{structurebold}
+
+\usepackage[english]{babel}
+\usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps}
+\usepackage{amsmath,amssymb}
+\usepackage[latin1]{inputenc}
+
+\setbeamercovered{dynamic}
+
+\newcommand{\Lang}[1]{\operatorname{\text{\textsc{#1}}}}
+
+\newcommand{\Class}[1]{\operatorname{\mathchoice
+ {\text{\sf \small #1}}
+ {\text{\sf \small #1}}
+ {\text{\sf #1}}
+ {\text{\sf #1}}}}
+
+\newcommand{\NumSAT} {\text{\small\#SAT}}
+\newcommand{\NumA} {\#_{\!A}}
+
+\newcommand{\barA} {\,\bar{\!A}}
+
+\newcommand{\Nat}{\mathbb{N}}
+\newcommand{\Set}[1]{\{#1\}}
+
+\pgfdeclaremask{tu}{beamer-tu-logo-mask}
+\pgfdeclaremask{computer}{beamer-computer-mask}
+\pgfdeclareimage[interpolate=true,mask=computer,height=2cm]{computerimage}{beamer-computer}
+\pgfdeclareimage[interpolate=true,mask=computer,height=2cm]{computerworkingimage}{beamer-computerred}
+\pgfdeclareimage[mask=tu,height=.5cm]{logo}{beamer-tu-logo}
+
+\logo{\pgfuseimage{logo}}
+
+\title{Weak Cardinality Theorems for First-Order Logic}
+\author{Till Tantau}
+\institute[Technische Universit\"at Berlin]{%
+ Fakultät für Elektrotechnik und Informatik\\
+ Technische Universit\"at Berlin}
+\date{Fundamentals of Computation Theory 2003}
+
+\colorlet{redshaded}{red!25!bg}
+\colorlet{shaded}{black!25!bg}
+\colorlet{shadedshaded}{black!10!bg}
+\colorlet{blackshaded}{black!40!bg}
+
+\colorlet{darkred}{red!80!black}
+\colorlet{darkblue}{blue!80!black}
+\colorlet{darkgreen}{green!80!black}
+
+\def\radius{0.96cm}
+\def\innerradius{0.85cm}
+
+\def\softness{0.4}
+\definecolor{softred}{rgb}{1,\softness,\softness}
+\definecolor{softgreen}{rgb}{\softness,1,\softness}
+\definecolor{softblue}{rgb}{\softness,\softness,1}
+
+\definecolor{softrg}{rgb}{1,1,\softness}
+\definecolor{softrb}{rgb}{1,\softness,1}
+\definecolor{softgb}{rgb}{\softness,1,1}
+
+\newcommand{\Bandshaded}[2]{
+ \color{shadedshaded}
+ \pgfmoveto{\pgfxy(-0.5,0)}
+ \pgflineto{\pgfxy(-0.6,0.1)}
+ \pgflineto{\pgfxy(-0.4,0.2)}
+ \pgflineto{\pgfxy(-0.6,0.3)}
+ \pgflineto{\pgfxy(-0.4,0.4)}
+ \pgflineto{\pgfxy(-0.5,0.5)}
+ \pgflineto{\pgfxy(4,0.5)}
+ \pgflineto{\pgfxy(4.1,0.4)}
+ \pgflineto{\pgfxy(3.9,0.3)}
+ \pgflineto{\pgfxy(4.1,0.2)}
+ \pgflineto{\pgfxy(3.9,0.1)}
+ \pgflineto{\pgfxy(4,0)}
+ \pgfclosepath
+ \pgffill
+
+ \color{black}
+ \pgfputat{\pgfxy(0,0.7)}{\pgfbox[left,base]{#1}}
+ \pgfputat{\pgfxy(0,-0.1)}{\pgfbox[left,top]{#2}}
+}
+
+\newcommand{\Band}[2]{
+ \color{shaded}
+ \pgfmoveto{\pgfxy(-0.5,0)}
+ \pgflineto{\pgfxy(-0.6,0.1)}
+ \pgflineto{\pgfxy(-0.4,0.2)}
+ \pgflineto{\pgfxy(-0.6,0.3)}
+ \pgflineto{\pgfxy(-0.4,0.4)}
+ \pgflineto{\pgfxy(-0.5,0.5)}
+ \pgflineto{\pgfxy(4,0.5)}
+ \pgflineto{\pgfxy(4.1,0.4)}
+ \pgflineto{\pgfxy(3.9,0.3)}
+ \pgflineto{\pgfxy(4.1,0.2)}
+ \pgflineto{\pgfxy(3.9,0.1)}
+ \pgflineto{\pgfxy(4,0)}
+ \pgfclosepath
+ \pgffill
+
+ \color{black}
+ \pgfputat{\pgfxy(0,0.7)}{\pgfbox[left,base]{#1}}
+ \pgfputat{\pgfxy(0,-0.1)}{\pgfbox[left,top]{#2}}
+}
+
+\newcommand{\BaenderNormal}
+{%
+ \pgfsetlinewidth{0.4pt}
+ \color{black}
+ \pgfputat{\pgfxy(0,5)}{\Band{input tapes}{}}
+ \pgfputat{\pgfxy(0.35,4.6)}{\pgfbox[center,base]{$\vdots$}}
+ \pgfputat{\pgfxy(0,4)}{\Band{}{}}
+
+ \pgfxyline(0,5)(0,5.5)
+ \pgfxyline(1.2,5)(1.2,5.5)
+ \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$w_1$}}
+
+ \pgfxyline(0,4)(0,4.5)
+ \pgfxyline(1.8,4)(1.8,4.5)
+ \pgfputat{\pgfxy(0.25,4.25)}{\pgfbox[left,center]{$w_n$}}
+ \ignorespaces}
+
+\newcommand{\BaenderZweiNormal}
+{%
+ \pgfsetlinewidth{0.4pt}
+ \color{black}
+ \pgfputat{\pgfxy(0,5)}{\Band{Zwei Eingabebänder}{}}
+ \pgfputat{\pgfxy(0,4.25)}{\Band{}{}}
+
+ \pgfxyline(0,5)(0,5.5)
+ \pgfxyline(1.2,5)(1.2,5.5)
+ \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$u$}}
+
+ \pgfxyline(0,4.25)(0,4.75)
+ \pgfxyline(1.8,4.25)(1.8,4.75)
+ \pgfputat{\pgfxy(0.25,4.5)}{\pgfbox[left,center]{$v$}}
+ \ignorespaces}
+
+\newcommand{\BaenderHell}
+{%
+ \pgfsetlinewidth{0.4pt}
+ \color{black}
+ \pgfputat{\pgfxy(0,5)}{\Bandshaded{input tapes}{}}
+ \color{shaded}
+ \pgfputat{\pgfxy(0.35,4.6)}{\pgfbox[center,base]{$\vdots$}}
+ \pgfputat{\pgfxy(0,4)}{\Bandshaded{}{}}
+
+ \color{blackshaded}
+ \pgfxyline(0,5)(0,5.5)
+ \pgfxyline(1.2,5)(1.2,5.5)
+ \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$w_1$}}
+
+ \pgfxyline(0,4)(0,4.5)
+ \pgfxyline(1.8,4)(1.8,4.5)
+ \pgfputat{\pgfxy(0.25,4.25)}{\pgfbox[left,center]{$w_n$}}
+ \ignorespaces}
+
+\newcommand{\BaenderZweiHell}
+{%
+ \pgfsetlinewidth{0.4pt}
+ \color{black}
+ \pgfputat{\pgfxy(0,5)}{\Bandshaded{Zwei Eingabebänder}{}}%
+ \color{blackshaded}
+ \pgfputat{\pgfxy(0,4.25)}{\Bandshaded{}{}}
+ \pgfputat{\pgfxy(0.25,4.5)}{\pgfbox[left,center]{$v$}}
+ \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$u$}}%
+
+ \pgfxyline(0,5)(0,5.5)
+ \pgfxyline(1.2,5)(1.2,5.5)
+
+ \pgfxyline(0,4.25)(0,4.75)
+ \pgfxyline(1.8,4.25)(1.8,4.75)
+ \ignorespaces}
+
+\newcommand{\Slot}[1]{%
+ \begin{pgftranslate}{\pgfpoint{#1}{0pt}}%
+ \pgfsetlinewidth{0.6pt}%
+ \color{structure}%
+ \pgfmoveto{\pgfxy(-0.1,5.5)}%
+ \pgfbezier{\pgfxy(-0.1,5.55)}{\pgfxy(-0.05,5.6)}{\pgfxy(0,5.6)}%
+ \pgfbezier{\pgfxy(0.05,5.6)}{\pgfxy(0.1,5.55)}{\pgfxy(0.1,5.5)}%
+ \pgflineto{\pgfxy(0.1,4.0)}%
+ \pgfbezier{\pgfxy(0.1,3.95)}{\pgfxy(0.05,3.9)}{\pgfxy(0,3.9)}%
+ \pgfbezier{\pgfxy(-0.05,3.9)}{\pgfxy(-0.1,3.95)}{\pgfxy(-0.1,4.0)}%
+ \pgfclosepath%
+ \pgfstroke%
+ \end{pgftranslate}\ignorespaces}
+
+\newcommand{\SlotZwei}[1]{%
+ \begin{pgftranslate}{\pgfpoint{#1}{0pt}}%
+ \pgfsetlinewidth{0.6pt}%
+ \color{structure}%
+ \pgfmoveto{\pgfxy(-0.1,5.5)}%
+ \pgfbezier{\pgfxy(-0.1,5.55)}{\pgfxy(-0.05,5.6)}{\pgfxy(0,5.6)}%
+ \pgfbezier{\pgfxy(0.05,5.6)}{\pgfxy(0.1,5.55)}{\pgfxy(0.1,5.5)}%
+ \pgflineto{\pgfxy(0.1,4.25)}%
+ \pgfbezier{\pgfxy(0.1,4.25)}{\pgfxy(0.05,4.15)}{\pgfxy(0,4.15)}%
+ \pgfbezier{\pgfxy(-0.05,4.15)}{\pgfxy(-0.1,4.2)}{\pgfxy(-0.1,4.25)}%
+ \pgfclosepath%
+ \pgfstroke%
+ \end{pgftranslate}\ignorespaces}
+
+\newcommand{\ClipSlot}[1]{%
+ \pgfrect[clip]{\pgfrelative{\pgfxy(-0.1,0)}{\pgfpoint{#1}{4cm}}}{\pgfxy(0.2,1.5)}\ignorespaces}
+
+\newcommand{\ClipSlotZwei}[1]{%
+ \pgfrect[clip]{\pgfrelative{\pgfxy(-0.1,0)}{\pgfpoint{#1}{4.25cm}}}{\pgfxy(0.2,1.25)}\ignorespaces}
+
+
+\AtBeginSection[]{\frame{\frametitle{Outline}\tableofcontents[current]}}
+
+\begin{document}
+
+\frame{\titlepage}
+
+%\section*{Outline}
+\part{Main Part}
+\frame{\frametitle{Outline}\tableofcontents[part=1]}
+
+\section{History}
+
+\subsection{Enumerability in Recursion and Automata Theory}
+
+\frame
+{
+ \frametitle{Motivation of Enumerability}
+
+ \begin{block}{Problem}
+ Many functions are not computable or not efficiently computable.
+ \end{block}
+ \vskip-1em
+ \begin{overprint}
+ \onslide<1-2>
+ \begin{example}
+ \begin{overprint}
+ \onslide<1>
+ \vskip0.5em
+ \begin{itemize}
+ \item
+ $\NumSAT$:\\
+ How many satisfying assignments does a formula have?
+ \end{itemize}
+
+ \onslide<2>
+ \vskip0.5em
+ For difficult languages~$A$:
+ \begin{itemize}
+ \item
+ Cardinality function $\NumA^n$:\\
+ \alert{How many} input words are in~$A$?
+ \item
+ Characteristic function $\chi_A^n$:\\
+ \alert{Which} input words are in~$A$?
+ \end{itemize}
+ \begin{pgfpicture}{-9cm}{0.75cm}{-9cm}{2cm}
+
+ \pgfnodebox{words}[virtual]{\pgfxy(0,3.5)}{$(w_1, \alert{w_2},
+ w_3, w_4, \alert{w_5})$}{2pt}{5pt}
+
+ \color{red}
+ \pgfputat{\pgfxy(0.75,4.5)}{\pgfbox[center,base]{in $A$}}
+ \pgfxyline(0.75,4.4)(-0.6,3.7)
+ \pgfxyline(0.75,4.4)(1.2,3.7)
+ \color{black}
+
+ \pgfnodebox{number}[virtual]{\pgfxy(-1,1)}{2}{2pt}{2pt}
+ \pgfnodebox{string}[virtual]{\pgfxy(1,1)}{0\alert{1}00\alert{1}}{2pt}{2pt}
+
+ \pgfsetstartarrow{\pgfarrowbar}
+ \pgfsetendarrow{\pgfarrowto}
+
+ \pgfnodeconnline{words}{string}%{-60}{120}{1cm}{1cm}
+ \pgfnodeconnline{words}{number}%{-120}{60}{1cm}{1cm}
+
+ \pgfputat{\pgfxy(-0.9,2.3)}{\pgfbox[center,base]{$\NumA^5$}}
+ \pgfputat{\pgfxy(0.9,2.3)}{\pgfbox[center,base]{$\chi_A^5$}}
+ \end{pgfpicture}
+ \end{overprint}
+ \end{example}
+
+ \onslide<3>
+ \begin{block}{Solutions}
+ Difficult functions can be
+ \begin{itemize}
+ \item
+ computed using probabilistic algorithms,
+ \item
+ computed efficiently on average,
+ \item
+ approximated, or
+ \item<alert at 1->
+ enumerated.
+ \end{itemize}
+ \end{block}
+ \end{overprint}
+}
+
+\frame
+{
+ \frametitle{Enumerators Output Sets of Possible Function Values}
+ \begin{columns}
+ \begin{column}{4.5cm}
+ \begin{pgfpicture}{-0.5cm}{0cm}{4cm}{6cm}
+
+ \pgfputat{\pgfxy(0,0.5)}{\Band{}{output tape}}
+
+ \BaenderHell
+
+ \color{black}
+
+ \only<1-4,6->{\pgfputat{\pgfxy(1.75,2.5)}{\pgfbox[center,center]{\pgfuseimage{computerimage}}}}
+ \only<5>{\pgfputat{\pgfxy(1.75,2.5)}{\pgfbox[center,center]{\pgfuseimage{computerworkingimage}}}}
+
+ \begin{pgfscope}
+ \only<1>{\ClipSlot{0cm}}
+ \only<2>{\ClipSlot{0.6cm}}
+ \only<3>{\ClipSlot{1.2cm}}
+ \only<4->{\ClipSlot{1.8cm}}
+ \BaenderNormal
+ \end{pgfscope}
+
+ \only<1>{\Slot{0cm}}
+ \only<2>{\Slot{0.6cm}}
+ \only<3>{\Slot{1.2cm}}
+ \only<4->{\Slot{1.8cm}}
+
+ \only<6->{
+ \pgfxyline(0,0.5)(0,1)
+ \pgfxyline(1,0.5)(1,1)
+ \pgfputat{\pgfxy(0.5,0.75)}{\pgfbox[center,center]{$u_1$}}}
+ \only<7->{
+ \pgfxyline(2,0.5)(2,1)
+ \pgfputat{\pgfxy(1.5,0.75)}{\pgfbox[center,center]{\alert<9>{$u_2$}}}}
+ \only<8->{
+ \pgfxyline(3,0.5)(3,1)
+ \pgfputat{\pgfxy(2.5,0.75)}{\pgfbox[center,center]{$u_3$}}}
+
+ \pgfsetlinewidth{0.6pt}
+ \color{structure}
+ \pgfsetendarrow{\pgfarrowto}
+
+ \pgfsetlinewidth{0.6pt}
+ \color{structure}
+ \pgfsetendarrow{\pgfarrowto}
+ \only<-5>{\pgfxycurve(1.75,1.5)(1.75,1)(0,1.5)(0,1.05)}
+ \only<6>{\pgfxycurve(1.75,1.5)(1.75,1)(1,1.5)(1,1.05)}
+ \only<7>{\pgfxycurve(1.75,1.5)(1.75,1)(2,1.5)(2,1.05)}
+ \only<8->{\pgfxycurve(1.75,1.5)(1.75,1)(3,1.5)(3,1.05)}
+
+ \only<1>{\pgfxycurve(1.75,3.5)(1.75,3.75)(0,3.5)(0,3.85)}
+ \only<2>{\pgfxycurve(1.75,3.5)(1.75,3.75)(0.6,3.5)(0.6,3.85)}
+ \only<3>{\pgfxycurve(1.75,3.5)(1.75,3.75)(1.2,3.5)(1.2,3.85)}
+ \only<4->{\pgfxycurve(1.75,3.5)(1.75,3.75)(1.8,3.5)(1.8,3.85)}
+ \end{pgfpicture}
+ \end{column}
+ \begin{column}{6.5cm}
+ \begin{definition}[1987, 1989, 1994, 2001]
+ An \alert{$m$-enumerator} for a function~$f$
+ \begin{enumerate}
+ \item<alert at 1-4>
+ reads $n$ input words $w_1$, \dots, $w_n$,
+ \item<alert at 5>
+ does a computation,
+ \item<alert at 6-8>
+ outputs at most $m$ values,
+ \item<alert at 9>
+ one of which is $f(w_1,\dots,w_n)$.
+ \end{enumerate}
+ \end{definition}
+ \end{column}
+ \end{columns}
+}
+
+\subsection{Known Weak Cardinality Theorem}
+
+\frame
+{
+ \frametitle{How Well Can the Cardinality Function Be Enumerated?}
+
+ \begin{block}{Observation}
+ For fixed~$n$, the cardinality function $\NumA^n$
+ \begin{itemize}
+ \item
+ can be \alert{$1$}-enumerated by Turing machines only for \alert{recursive}~$A$,~but\hskip-0.5cm\hbox{}
+ \item
+ can be \alert{$(n+1)$}-enumerated for \alert{every} language~$A$.
+ \end{itemize}
+ \end{block}
+
+ \begin{alertblock}{Question}<2->
+ What about $2$-, $3$-, $4$-, \dots, $n$-enumerability?
+ \end{alertblock}
+}
+
+\newtheorem{card}{Cardinality Theorem}[theorem]
+\newtheorem{weakcard}{Weak Cardinality Theorems}[theorem]
+
+\frame
+{
+ \frametitle{How Well Can the Cardinality Function\\ Be Enumerated
+ by Turing Machines?}
+
+ \begin{card}[Kummer, 1992]
+ If $\NumA^n$ is $n$-enumerable by a Turing machine, then $A$ is
+ recursive.
+ \end{card}
+
+ \begin{weakcard}[\uncover<2->{\alert<1-2>{1987},} \uncover<3->{\alert<3>{1989},}
+ \uncover<4->{\alert<4>{1992}}]<2->
+ \begin{enumerate}
+ \item<2-| alert at 2>
+ If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$ is
+ recursive.
+ \item<3-| alert at 3>
+ If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$ is
+ recursive.
+ \item<4-| alert at 4>
+ If $\NumA^n$ is $n$-enumerable by a Turing machine that never
+ enumerates both $0$ and~$n$, then $A$ is recursive.
+ \end{enumerate}
+ \end{weakcard}
+}
+
+
+\frame
+{
+ \frametitle{How Well Can the Cardinality Function\\ Be Enumerated
+ by Finite Automata?}
+
+ \begin{alertblock}{Conjecture}
+ If $\NumA^n$ is $n$-enumerable by a \alert{finite automaton}, then $A$ is
+ \alert{regular}.
+ \end{alertblock}
+
+ \begin{weakcard}[2001, 2002]
+ \begin{enumerate}
+ \item
+ If $\chi_A^n$ is $n$-enumerable by a \alert{finite automaton}, then $A$ is
+ \alert{regular}.
+ \item
+ If $\NumA^2$ is $2$-enumerable by a \alert{finite automaton}, then $A$ is
+ \alert{regular}.
+ \item
+ If $\NumA^n$ is $n$-enumerable by a \alert{finite automaton} that never
+ enumerates both $0$ and~$n$, then $A$ is \alert{regular}.
+ \end{enumerate}
+ \end{weakcard}
+}
+
+
+\subsection{Why Do Cardinality Theorems Hold Only for Certain Models?}
+
+\frame
+{
+ \frametitle{Cardinality Theorems Do Not Hold for All Models}
+
+ \begin{pgfpicture}{-2.5cm}{0.3cm}{0.5cm}{6.5cm}
+ \pgfsetlinewidth{0.6pt}
+
+ \pgfsetendarrow{\pgfarrowto}
+ \pgfxyline(0,0.5)(0,6.5)
+ \pgfclearendarrow
+
+ \pgfputat{\pgfxy(-0.2,5.75)}{\pgfbox[right,base]{Turing machines}}
+
+ \only<2>{
+ \pgfputat{\pgfxy(-0.2,3.75)}{\pgfbox[right,base]{\alert{resource-bounded}}}
+ \pgfputat{\pgfxy(-0.2,3.25)}{\pgfbox[right,base]{\alert{machines}}}
+ \pgfcircle[fill]{\pgfxy(0,3.6)}{2pt}
+ \pgfputat{\pgfxy(0.4,3.5)}{\pgfbox[left,base]{Weak cardinality
+ theorems do \alert{not} hold.}}}
+
+ \pgfputat{\pgfxy(-0.2,1.5)}{\pgfbox[right,base]{finite}}
+ \pgfputat{\pgfxy(-0.2,1)}{\pgfbox[right,base]{automata}}
+
+ \pgfcircle[fill]{\pgfxy(0,5.85)}{2pt}
+ \pgfcircle[fill]{\pgfxy(0,1.35)}{2pt}
+
+ \pgfputat{\pgfxy(0.4,5.75)}{\pgfbox[left,base]{Weak cardinality
+ theorems hold.}}
+ \pgfputat{\pgfxy(0.4,1.25)}{\pgfbox[left,base]{Weak cardinality
+ theorems hold.}}
+ \end{pgfpicture}
+}
+
+\frame
+{
+ \frametitle{Why?}
+
+ \begin{block}{First Explanation}<1>
+ The weak cardinality theorems hold both for recursion and automata
+ theory \alert{by coincidence}.
+ \end{block}
+
+ \begin{block}{Second Explanation}<1-2>
+ The weak cardinality theorems hold both for
+ recursion and automata theory, \alert{because they are
+ instantiations of\\ single, unifying theorems}.
+ \end{block}
+
+ \vskip1em
+ \visible<2->{
+ The second explanation is correct.\\
+ The theorems can (almost) be unified using first-order logic.
+ }
+}
+
+
+
+\section[Unification by Logic]{Unification by First-Order Logic}
+
+\subsection{Elementary Definitions}
+
+\frame
+{
+ \frametitle{What Are Elementary Definitions?}
+
+ \begin{definition}
+ A relation~$R$ is \alert{elementarily definable in a
+ logical structure~$\mathcal S$} if
+ \begin{enumerate}
+ \item
+ there exists a first-order formula~$\phi$,
+ \item
+ that is true exactly for the elements of~$R$.
+ \end{enumerate}
+ \end{definition}
+
+ \begin{example}
+ The set of even numbers is elementarily definable in $(\Nat, +)$
+ via the formula $\phi(x) \equiv \exists z \centerdot z+z=x$.
+ \end{example}
+
+ \begin{example}
+ The set of powers of 2 is not elementarily definable in $(\Nat, +)$.
+ \end{example}
+}
+
+
+\frame
+{
+ \frametitle{Characterisation of Classes by Elementary Definitions}
+
+ \begin{theorem}[B\"uchi, 1960]
+ There exists a logical structure~$(\Nat, +, \mathrm e_2)$
+ such that a set $A \subseteq \Nat$ is\\ \alert{regular} iff it is
+ \alert{elementarily definable in~$(\Nat, +, \mathrm e_2)$}.
+ \end{theorem}
+
+ \begin{theorem}
+ There exists a logical structure~$\mathcal R$ such that a set $A
+ \subseteq \Nat$ is \alert{recursively enumerable} iff it is \alert{positively
+ elementarily definable in~$\mathcal R$}.\hskip-0.5cm\hbox{}
+ \end{theorem}
+}
+
+
+
+\frame
+{
+ \frametitle{Characterisation of Classes by Elementary Definitions}
+
+ \begin{pgfpicture}{-5.4cm}{0.3cm}{5.4cm}{6.5cm}
+ \pgfsetlinewidth{0.6pt}
+
+ \pgfsetendarrow{\pgfarrowto}
+ \pgfxyline(0,0.3)(0,6.5)
+ \pgfclearendarrow
+
+ \only<2->{
+ \pgfputat{\pgfxy(-0.3,0.5)}{\pgfbox[right,base]{Presburger arithmetic}}
+ \pgfcircle[fill]{\pgfxy(0,0.6)}{2pt}
+ \pgfputat{\pgfxy(0.3,0.5)}{\pgfbox[left,base]{$(\Nat, +)$}}
+ }
+ \pgfputat{\pgfxy(-0.3,1.5)}{\pgfbox[right,base]{regular sets}}
+ \pgfcircle[fill]{\pgfxy(0,1.6)}{2pt}
+ \pgfputat{\pgfxy(0.3,1.5)}{\pgfbox[left,base]{$(\Nat, +, \mathrm e_2)$}}
+
+ \pgfputat{\pgfxy(-0.3,2.5)}{\pgfbox[right,base]{\alert{resource-bounded classes}}}
+ \pgfcircle[fill]{\pgfxy(0,2.6)}{2pt}
+ \pgfputat{\pgfxy(0.3,2.5)}{\pgfbox[left,base]{\alert{none}}}
+
+ \pgfputat{\pgfxy(-0.3,3.5)}{\pgfbox[right,base]{recursively enumerable sets}}
+ \pgfcircle[fill]{\pgfxy(0,3.6)}{2pt}
+ \pgfputat{\pgfxy(0.3,3.5)}{\pgfbox[left,base]{positively in $\mathcal R$}}
+
+ \only<2->{
+ \pgfputat{\pgfxy(-0.3,4.5)}{\pgfbox[right,base]{arithmetic hierarchy}}
+ \pgfcircle[fill]{\pgfxy(0,4.6)}{2pt}
+ \pgfputat{\pgfxy(0.3,4.5)}{\pgfbox[left,base]{$(\Nat, +, \cdot)$}}
+
+ \pgfputat{\pgfxy(-0.3,5.5)}{\pgfbox[right,base]{ordinal number arithmetic}}
+ \pgfcircle[fill]{\pgfxy(0,5.6)}{2pt}
+ \pgfputat{\pgfxy(0.3,5.5)}{\pgfbox[left,base]{$(\mathrm{On}, +, \cdot)$}}}
+ \end{pgfpicture}
+}
+
+
+\subsection{Enumerability for First-Order Logic}
+
+\frame
+{
+ \frametitle{Elementary Enumerability is a Generalisation of\\ Elementary Definability}
+
+ \begin{columns}
+ \begin{column}{3.25cm}
+ \begin{pgfpicture}{-0.25cm}{0cm}{3cm}{4cm}
+
+ \color{shaded}
+ \pgfmoveto{\pgfxy(0,1.3)}
+ \pgfcurveto{\pgfxy(0.5,2.3)}{\pgfxy(2,1.5)}{\pgfxy(2.5,2.3)}
+ \pgflineto{\pgfxy(2.5,1.7)}
+ \pgfcurveto{\pgfxy(2,0.7)}{\pgfxy(1,1.7)}{\pgfxy(0,0.5)}
+ \pgfclosepath
+ \pgffill
+
+ \pgfsetlinewidth{0.8pt}
+ \color{black}
+ \pgfmoveto{\pgfxy(0,1)}
+ \pgflineto{\pgfxy(0.25,1.15)}
+ \pgflineto{\pgfxy(0.5,1.5)}
+ \pgflineto{\pgfxy(1,1.7)}
+ \pgflineto{\pgfxy(1.5,1.5)}
+ \pgflineto{\pgfxy(2,1.4)}
+ \pgflineto{\pgfxy(2.25,1.5)}
+ \pgflineto{\pgfxy(2.5,2)}
+ \pgfstroke
+
+ \pgfsetlinewidth{0.4pt}
+ \pgfsetendarrow{\pgfarrowto}
+ \pgfxyline(0,0)(2.5,0)
+ \pgfxyline(0,0)(0,3)
+ \pgfputat{\pgfxy(0.5,1.9)}{\pgfbox[center,base]{$R$}}
+ \pgfputat{\pgfxy(2.6,0)}{\pgfbox[left,center]{$x$}}
+ \pgfputat{\pgfxy(0,3.2)}{\pgfbox[center,base]{$f(x)$}}
+ \pgfputat{\pgfxy(2.55,2)}{\pgfbox[left,center]{$f$}}
+ \end{pgfpicture}
+ \end{column}
+ \begin{column}{7.5cm}
+ \begin{definition}
+ A function~$f$ is\\
+ \alert{elementarily $m$-enumerable in a structure~$\mathcal S$} if
+ \begin{enumerate}
+ \item
+ its graph is contained in an\\
+ \alert{elementarily definable} relation~$R$,
+ \item
+ which is \alert{$m$-bounded}, i.\kern1pt e., for each~$x$
+ there are at most~$m$ different~$y$ with $(x,y) \in R$.
+ \end{enumerate}
+ \end{definition}
+ \end{column}
+ \end{columns}
+}
+
+\frame
+{
+ \frametitle{The Original Notions of Enumerability are Instantiations}
+
+ \begin{theorem}
+ A function is $m$-enumerable by a \alert{finite automaton} iff\\
+ it is elementarily $m$-enumerable in \alert{$(\Nat, +, \mathrm e_2)$}.
+ \end{theorem}
+
+ \begin{theorem}
+ A function is $m$-enumerable by a \alert{Turing machine} iff\\
+ it is positively elementarily $m$-enumerable in \alert{$\mathcal R$}.
+ \end{theorem}
+}
+
+%\subsection{Cross Product Theorem for First-Order Logic}
+
+\subsection{Weak Cardinality Theorems for First-Order Logic}
+
+\frame
+{
+ \frametitle{The First Weak Cardinality Theorem}
+
+ \begin{theorem}
+ Let $\mathcal S$ be a logical structure with universe~$U$ and let
+ $A \subseteq U$. If
+
+ \begin{enumerate}
+ \item
+ $\mathcal S$ is well-orderable and
+ \item
+ \alert{$\chi_A^n$} is elementarily \alert{$n$}-enumerable in~$\mathcal S$,
+ \end{enumerate}
+
+ then \alert{$A$ is elementarily definable} in~$\mathcal S$.
+ \end{theorem}
+ \begin{overprint}
+ \onslide<2>
+ \begin{corollary}
+ If $\chi_A^n$ is $n$-enumerable by a finite automaton, then
+ $A$ is regular.
+ \end{corollary}
+
+ \onslide<3>
+ \begin{corollary}[with more effort]
+ If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$
+ is recursive.
+ \end{corollary}
+ \end{overprint}
+}
+
+\frame
+{
+ \frametitle{The Second Weak Cardinality Theorem}
+
+ \begin{theorem}
+ Let $\mathcal S$ be a logical structure with universe~$U$ and let
+ $A \subseteq U$. If
+
+ \begin{enumerate}
+ \item
+ $\mathcal S$ is well-orderable,
+ \item
+ every finite relation on~$U$ is elementarily definable
+ in~$\mathcal S$, and
+ \item
+ \alert{$\NumA^2$} is elementarily \alert{$2$}-enumerable in~$\mathcal S$,
+ \end{enumerate}
+
+ then \alert{$A$ is elementarily definable} in~$\mathcal S$.
+ \end{theorem}
+% \begin{overlayarea}{\textwidth}{2cm}
+% \only<2>{
+% \begin{corollary}
+% If $\NumA^2$ is $2$-enumerable by a finite automaton, then
+% $A$ is regular.
+% \end{corollary}}%
+% \only<3>{
+% \begin{block}{Corollary}
+% If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$
+% is recursive in the halting problem.
+% \end{block}
+% }
+% \end{overlayarea}
+}
+
+\frame
+{
+ \frametitle{The Third Weak Cardinality Theorem}
+
+ \begin{theorem}
+ Let $\mathcal S$ be a logical structure with universe~$U$ and let
+ $A \subseteq U$. If
+
+ \begin{enumerate}
+ \item
+ $\mathcal S$ is well-orderable,
+ \item
+ every finite relation on~$U$ is elementarily definable
+ in~$\mathcal S$, and
+ \item
+ \alert{$\NumA^n$} is elementarily \alert{$n$}-enumerable in~$\mathcal S$ via a
+ relation that \alert{never `enumerates' both $0$ and~$n$},
+ \end{enumerate}
+
+ then \alert{$A$ is elementarily definable} in~$\mathcal S$.
+ \end{theorem}
+% \begin{overlayarea}{\textwidth}{2cm}
+% \only<2>{
+% \begin{corollary}
+% If $\NumA^n$ is $n$-enumerable by a finite automaton that
+% never enumerates both $0$ and~$n$, then $A$ is regular.
+% \end{corollary}}%
+% \only<3>{
+% \begin{block}{Corollary}
+% If $\NumA^n$ is $n$-enumerable by a Turing machine that never
+% enumerates both $0$ and~$n$, then $A$ is recursive in the
+% halting problem.
+% \end{block}
+% }
+% \end{overlayarea}
+}
+
+
+
+\frame
+{
+ \frametitle{Relationships Between Cardinality Theorems (CT)}
+
+ \begin{pgfpicture}{0cm}{0cm}{10cm}{5cm}
+ \only<2>{%
+ \color{alert}
+ \pgfnodebox{autX}[virtual]{\pgfxy(2.2,4)}{CT}{2pt}{2pt}
+ \color{black}}%
+ \pgfnodebox{autA}[virtual]{\pgfxy(1,3)}{1st Weak CT}{2pt}{2pt}
+ \pgfnodebox{autB}[virtual]{\pgfxy(1,2)}{2nd Weak CT}{2pt}{2pt}
+ \pgfnodebox{autC}[virtual]{\pgfxy(1,1)}{3rd Weak CT}{2pt}{2pt}
+
+ \only<2>{%
+ \color{alert}
+ \pgfnodebox{logX}[virtual]{\pgfxy(6.2,4.5)}{CT}{2pt}{2pt}%
+ \color{black}}%
+ \pgfnodebox{logA}[virtual]{\pgfxy(5,3.5)}{1st Weak CT}{2pt}{2pt}
+ \pgfnodebox{logB}[virtual]{\pgfxy(5,2.5)}{2nd Weak CT}{2pt}{2pt}
+ \pgfnodebox{logC}[virtual]{\pgfxy(5,1.5)}{3rd Weak CT}{2pt}{2pt}
+
+ \pgfnodebox{recX}[virtual]{\pgfxy(10.2,4)}{CT}{2pt}{2pt}
+ \pgfnodebox{recA}[virtual]{\pgfxy(9,3)}{1st Weak CT}{2pt}{2pt}
+ \pgfnodebox{recB}[virtual]{\pgfxy(9,2)}{2nd Weak CT}{2pt}{2pt}
+ \pgfnodebox{recC}[virtual]{\pgfxy(9,1)}{3rd Weak CT}{2pt}{2pt}
+
+ \pgfputat{\pgfxy(1,4.5)}{\pgfbox[center,base]{\structure{automata theory}}}
+ \pgfputat{\pgfxy(5,5)}{\pgfbox[center,base]{\structure{first-order logic}}}
+ \pgfputat{\pgfxy(9,4.5)}{\pgfbox[center,base]{\structure{recursion
+ theory}}}
+
+ {%
+ \color{structure}%
+ \pgfxyline(3,0)(3,5)
+ \pgfxyline(7,0)(7,5)
+ }%
+ \pgfsetendarrow{\pgfarrowto}
+ \pgfnodeconnline{logA}{autA}
+ \pgfnodeconnline{logA}{recA}
+ \pgfnodeconnline{logB}{autB}
+ \pgfnodeconnline{logC}{autC}
+
+ \pgfnodeconncurve{recX}{recA}{-60}{5}{10pt}{10pt}
+ \pgfnodeconncurve{recX}{recB}{-55}{5}{10pt}{20pt}
+ \pgfnodeconncurve{recX}{recC}{-50}{5}{10pt}{30pt}
+
+ \only<2>{%
+ \alert{
+ \pgfnodeconnline{logX}{autX}
+ \pgfnodeconncurve{logX}{logA}{-60}{0}{10pt}{10pt}
+ \pgfnodeconncurve{logX}{logB}{-55}{0}{10pt}{20pt}
+ \pgfnodeconncurve{logX}{logC}{-50}{0}{10pt}{30pt}
+ \pgfnodeconncurve{autX}{autA}{-60}{11}{10pt}{10pt}
+ \pgfnodeconncurve{autX}{autB}{-55}{11}{10pt}{20pt}
+ \pgfnodeconncurve{autX}{autC}{-50}{11}{10pt}{30pt}
+ }
+ }
+
+ \pgfsetdash{{3pt}{3pt}}{0pt}
+ \pgfnodeconnline{logB}{recB}
+ \pgfnodeconnline{logC}{recC}
+
+ \only<2>{%
+ \alert{\pgfnodeconnline{logX}{recX}}}
+ \end{pgfpicture}
+}
+
+
+\section{Applications}
+
+\subsection{A Separability Result for First-Order Logic}
+
+%\frame
+%{
+% \begin{columns}
+% \begin{column}{2.4cm}
+% \begin{pgfpicture}{-1.2cm}{-1.2cm}{1cm}{1cm}
+% \color{shaded}
+% \pgfrect[fill]{\pgfxy(-1.4,-1)}{\pgfxy(2.8,2)}
+
+% \color{white}
+% \pgfcircle[fill]{\pgfxy(-0.6,0)}{0.5cm}
+% \pgfcircle[fill]{\pgfxy(0.6,0)}{0.5cm}
+% \only<2->{%
+% \color{softred}
+% \pgfcircle[fill]{\pgfxy(-0.6,0)}{0.6cm}}%
+% %
+% \color{black}
+% \pgfcircle[stroke]{\pgfxy(-0.6,0)}{0.5cm}
+% \pgfcircle[stroke]{\pgfxy(0.6,0)}{0.5cm}
+
+% \pgfputat{\pgfxy(-0.6,0)}{\pgfbox[center,center]{$A^{(n)}$}}
+% \pgfputat{\pgfxy(0.6,0)}{\pgfbox[center,center]{$\barA{}^{(n)}$}}
+% \end{pgfpicture}
+% \end{column}
+% \begin{column}{8cm}
+% \begin{block}{Notation}
+% Let $A^{(n)}$ contain all $n$ tuples of\\
+% distinct elements of~$A$.
+% \end{block}
+
+% \begin{block}{Theorem}
+% Let $\mathcal S$ be a well-orderable logical structure in which
+% all finite relations are elementarily definable.\\[0.5em]
+% If $A^{(n)}$ and $\barA{}^{(n)}$ are \alert<2>{elementarily separable}
+% in~$\mathcal S$, then~so~are~$A$~and~$\barA$.
+% \end{block}
+
+% \uncover<3>{
+% \begin{alertblock}{Note}
+% The theorem is no longer true if $\barA$ is replaced by an
+% arbitrary set~$B$.
+% \end{alertblock}
+% }
+% \end{column}
+% \end{columns}
+%}
+
+
+\frame
+{
+ \begin{columns}
+ \begin{column}{4cm}
+ \begin{pgfpicture}{-2cm}{-1.75cm}{2cm}{2.25cm}
+ \color{shaded}
+ \pgfrect[fill]{\pgfxy(-2,-1.75)}{\pgfxy(4,4)}
+ %\pgfcircle[fill]{\pgforigin}{2cm}
+
+ \only<1>{%
+ \color{white}%
+ \pgfcircle[fill]{\pgfpolar{90}{1cm}}{\innerradius}
+ \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\innerradius}
+ \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\innerradius}}%
+ \only<2->{%
+ \color{softred}
+ \pgfcircle[fill]{\pgfpolar{90}{1cm}}{\radius}
+ \color{softgreen}
+ \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\radius}
+ \color{softblue}
+ \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}}%
+ %
+ \only<2->{%
+ \begin{pgftranslate}{\pgfpolar{90}{1cm}}
+ \pgfzerocircle{\radius}
+ \pgfclip
+
+ \begin{pgftranslate}{\pgfpolar{-90}{1cm}}
+ \color{softrb}
+ \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}
+ \color{softrg}
+ \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\radius}
+ \end{pgftranslate}
+ \end{pgftranslate}
+
+ \begin{pgftranslate}{\pgfpolar{210}{1cm}}
+ \pgfzerocircle{\radius}
+ \pgfclip
+
+ \begin{pgftranslate}{\pgfpolar{30}{1cm}}
+ \color{softgb}
+ \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}
+ \end{pgftranslate}
+ \end{pgftranslate}}%
+ %
+ \color{black}
+ \pgfcircle[stroke]{\pgfpolar{90}{1cm}}{\innerradius}
+ \pgfcircle[stroke]{\pgfpolar{210}{1cm}}{\innerradius}
+ \pgfcircle[stroke]{\pgfpolar{330}{1cm}}{\innerradius}
+
+ \pgfputat{\pgfrelative{\pgfpolar{90}{1cm}}%
+ {\pgfpoint{0pt}{-.5ex}}}%
+ {\pgfbox[center,base]{$A\times \barA$}}
+ \pgfputat{\pgfrelative{\pgfpolar{210}{1cm}}%
+ {\pgfpoint{0pt}{-.5ex}}}%
+ {\pgfbox[center,base]{$A\times A$}}
+ \pgfputat{\pgfrelative{\pgfpolar{330}{1cm}}%
+ {\pgfpoint{0pt}{-.5ex}}}%
+ {\pgfbox[center,base]{$\barA\times \barA$}}
+
+ \end{pgfpicture}
+ \end{column}
+ \begin{column}{6.8cm}
+ \begin{theorem}
+ Let $\mathcal S$ be a well-orderable logical structure in which
+ all finite relations are elementarily definable.\\[0.5em]
+ If there exist elementarily definable supersets of
+ {\color<2>{darkgreen}$A \times A$},
+ {\color<2>{darkred}$A \times \barA$}, and
+ {\color<2>{darkblue}$\barA \times \barA$} whose
+ intersection is empty,\\
+ then $A$ is elementarily definable in~$\mathcal S$.
+ \end{theorem}
+ \begin{alertblock}{Note}<3>
+ The theorem is no longer true\\
+ if we add $\barA \times A$ to the list.
+ \end{alertblock}%
+ \end{column}
+ \end{columns}
+}
+
+
+\section*{Summary}
+
+\frame
+{
+ \frametitle{Summary}
+
+ \begin{block}{Summary}
+ \begin{itemize}
+ \item
+ The weak cardinality theorems for first-order logic \alert{unify}\\
+ the weak cardinality theorems of automata and recursion theory.
+ \item
+ The logical approach yields
+ weak cardinality theorems for\\ \alert{other computational models}.
+ \item
+ Cardinality theorems are \alert{separability theorems} in disguise.
+ \end{itemize}
+ \end{block}{}
+
+ \begin{block}{Open Problems}
+ \begin{itemize}
+ \item
+ Does a cardinality theorem for first-order logic hold?
+ \item
+ What about non-well-orderable structures like $(\mathbb R, +,
+ \cdot)$?
+ \end{itemize}
+ \end{block}
+}
+
+\end{document}
+
+
More information about the Pkg-tetex-commits
mailing list