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, 0 insertions, 1021 deletions
diff --git a/Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex b/Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex deleted file mode 100644 index 23ef834d70e..00000000000 --- a/Master/texmf-dist/doc/latex/beamer/examples/beamerexample5.tex +++ /dev/null @@ -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@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} - - |