diff options
Diffstat (limited to 'Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex')
-rw-r--r-- | Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex | 1021 |
1 files changed, 1021 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex b/Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex new file mode 100644 index 00000000000..23ef834d70e --- /dev/null +++ b/Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex @@ -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@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@1-4> + reads $n$ input words $w_1$, \dots, $w_n$, + \item<alert@5> + does a computation, + \item<alert@6-8> + outputs at most $m$ values, + \item<alert@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@2> + If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$ is + recursive. + \item<3-| alert@3> + If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$ is + recursive. + \item<4-| alert@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} + + |