\documentclass{beamer}

\usetheme{Warsaw}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage[portuguese]{babel}
\input xy
\xyoption{all}

\title{Máquina de Post}
\author{BORTOLINI D., GALLOIS F., FREITAS L.F., SANTOS R.}
\institute{UDESC - Universidade do Estado de Santa Catarina}
\date{16 de Julho de 2008}

\begin{document}
\maketitle

% Emil Post
\begin{frame}
\frametitle{Emil Post}
	\begin{itemize}
	\item Matemático e Lógico
	\item Nascido em 1897, Augustów, antigo Império Russo (atual Polônia)
	\item Morreu em 1954, NYC
	\item Criado nos Estados Unidos, fez seu pós-doutorado em Princeton
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Emil Post}
	\begin{itemize}
	\item Em 1936 (na verdade, o artigo é de 1935, mas só foi publicado em 1936), desenvolveu um modelo computacional que é essencialmente equivalente à Máquina de Turing, muito embora os trabalhos tenham sido feitos independentemente.
	\item Esse modelo seria o primeiro de uma série que envolveria outros de mesmo poder computacional, mas com complexidade crescente. O trabalho foi entitulado "Formulation 1" (máquina de Post).
	\end{itemize}
\end{frame}

% Decidibilidade
\begin{frame}
\frametitle{Decidibilidade}
	\begin{itemize}
	\item Post estava preocupado em mostrar a decidibilidade dos problemas.
\pause
	\item Um problema de decisão é um problema genérico que consiste de uma classe de problemas específicos.
\pause
	\item Um problema de decisão admite somente dois valores como resposta (do tipo sim-ou-não).
\pause
	\item Um problema é considerado decidível se, e somente se, existe um procedimento genérico no qual, quando aplicado a cada um dos casos específicos, resulta em uma solução para cada um dos casos.
\pause
	\item Um problema de decisão que pode ser resolvido por um algoritmo, é dito decidível.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Decidibilidade}
	\begin{itemize}
	\item Um exemplo de problema decidível é um onde devemos determinar, para dois inteiros arbitrários $x$ e $y$, se $x$ é um divisor de $y$.
\pause
	\item Um exemplo de problema indecidível é um onde, dada uma máquina de Turing saber se ela vai parar ou não.
\pause
	\item Post entendia sua formulação como capaz de resolver qualquer problema de decisão que fosse considerado intuitivamente decidível, assim como as máquinas de Turing são reconhecidas por serem capazes de computar qualquer coisa que seja intuitivamente computável.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Decidibilidade}
	\begin{itemize}
	\item Como absorver formalmente a noção de decidibilidade? A resposta de Post estava no que originalmente chamou de "Formulation 1".
	\end{itemize}
\end{frame}

% Máquina de Post
\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item Em sua formulação genérica para solução de problemas decidíveis existem dois conceitos envolvidos: um symbol space (fita) onde o trabalho à caminho da solução será feito e um conjunto de instruções onde que dirige as operações sore o symbol space e determina a ordem na qual as direções devem ser executadas.
	\item Symbol space é uma sequência de células (cells, boxes). O worker (cabeça) pode se mover e trabalhar no symbol space, e e capaz de estar e trabalhar em uma célula, mas apenas em uma de cada vez.
	\item Uma célula tem duas condições possíveis, vazia ou marcada com um símbolo. Uma das células será o ponto de início.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item O worker pode executar apenas as seguintes ações
		\begin{enumerate}[(a)]
		\item Marcar a célula em que se encontra (assumindo que esta esteja vazia)
\pause
		\item Apagar a marca na célula em que se econtra (assumindo que esteja marcada)
\pause
		\item Mover-se para a célula à direita
\pause
		\item Mover-se para a célula à esquerda
\pause
		\item Dizer se a célula em que se encontra está ou não marcada.
\pause
		\item Parar
		\end{enumerate}
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item As ações dos workers são ordenadas através de um conjunto de instruções, que deve permancer inalterado para todos os casos específicos do problema de decidibilidade que se deseja resolver. Isso garantirá que o conjunto de instruções seja genérico. Para o caso da divisão por inteiros, o conjunto de instruções na máquina de Post deverá ser o mesmo para todo par específico de inteiros.
	\item As máquinas de Post comportam-se de maneira análoga às maquinas de Turing nesse aspecto. Elas percorrem a fita executando instruções, tal qual as máquinas de Turing.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
Abaixo uma demonstração de como deve proceder uma máquina de Post\\
\pause
Partindo do ponto inicial, seguindo a instrução 1.\\
\pause
Deve haver um numero finito de instruções a serem numeradas $1,2,3,...,n$. A $i$-ésima instrução deve então ter uma das seguintes formas:
\pause
	\begin{enumerate}[(A)]
	\item \textit{Realizar a operação $O_i[O_i = (a), (b), (c), ou (d)]$ e então seguir a instrução $j_i$,}\\
\pause
	\item \textit{Realizar a operação $(e)$ e de acordo com a resposta, sim ou não, seguir a instrução $j_i'$ ou $j_i''$,}\\
\pause
	\item \textit{Parar.}
	\end{enumerate}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item As definições anteriores sugerem que, em uma determinada célula, o worker pode:
		\begin{enumerate}
		\item Marcar uma célula
		\item Apagar uma célula
		\item Mover para a célula à direita
		\item Mover para a célula à esquerda
		\end{enumerate}
	\item Alternativamente, ele pode analisar o estado da célula e, com base no resultado, seguir uma instrução.
	\item Esse tipo de instrução garante uma característica de condicionalidade da instrução seguinte.
	\item Finalmente, a máquina pode parar.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
Vejamos abaixo uma representação das instruções visando maior clareza dos conceitos ($i$ é a instrução e $j$ é o jump, próxima instrução a ser executada)
\pause
	\begin{enumerate}[(a)]
	\item Marcar a célula em que se encontra (assumindo que esta esteja vazia)
		\begin{center}
		\begin{displaymath}
		i.\,\vee\,j.
		\end{displaymath}
		\end{center}
\pause
	\item Apagar a marca na célula em que se econtra (assumindo que esteja marcada)
		\begin{center}
		\begin{displaymath}
		i.\;\xi\;j.
		\end{displaymath}
		\end{center}
	\end{enumerate}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{enumerate}[(c)]
	\item Mover-se para a célula à direita
		\begin{center}
		\begin{displaymath}
		\xymatrix{i. \ar@2{->}[r] & j.}
		\end{displaymath}
		\end{center}
	\end{enumerate}
\pause
	\begin{enumerate}[(d)]
	\item Mover-se para a célula à esquerda
		\begin{center}
		\begin{displaymath}
		\xymatrix{i. \ar@2{<-}[r] & j.}
		\end{displaymath}
		\end{center}
	\end{enumerate}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{enumerate}[(e)]
	\item Dizer se a célula em que se encontra está ou não marcada.
		\begin{center}
		\begin{displaymath}
		\xymatrix{ 	& & j'.\\
					i. & ?  \ar@{-}[ur] \ar@{-}[dr] & \\
					& & j''.}
		\end{displaymath}
		\end{center}
	\end{enumerate}
\pause
	\begin{enumerate}[(f)]
	\item Parar
		\begin{center}
		\begin{displaymath}
		i. stop.
		\end{displaymath}
		\end{center}
	\end{enumerate}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
Veja alguns exemplos do funcionamento de uma Máquina de Post no quadro \\
Exemplo 1:
	\begin{itemize}
	\item $1. \vee 4 $
	\item $2. \xi 3 $
	\item $\xymatrix{3. \ar@2{<-}[r] & 2}$
	\item $\xymatrix{4. \ar@2{->}[r] & 5}$
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item $\xymatrix{ 	& & 4\\
					5. & ?  \ar@{-}[ur] \ar@{-}[dr] & \\
					& & 3}$
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
Exemplo 2:
	\begin{itemize}
	\item $1. \vee 4 $
	\item $2. \;stop $
	\item $\xymatrix{3. \ar@2{<-}[r] & 2}$
	\item $\xymatrix{4. \ar@2{->}[r] & 5}$
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item $\xymatrix{ 	& & 4\\
					5. & ?  \ar@{-}[ur] \ar@{-}[dr] & \\
					& & 3}$
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
Os dois exemplos abaixo mostram máquinas que rodariam infinitamente
	\begin{itemize}
 	\item $\xymatrix{1. \ar@2{->}[r] & 1}$
	\item $\xymatrix{ 	& & 1\\
					1. & ?  \ar@{-}[ur] \ar@{-}[dr] & \\
					& & 1}$
	\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item A formulação de Post seria, de acordo com ele, capaz de resolver qualquer prolema intuitivamente resolvível.
	\item Um problema que não possa ser resolvido ao usar-se um determinado conjunto de instruções sobre uma entrada, gerando uma solução diferente para cada caso específico do problema deve ser considerado não resolvível.
	\item Após descrever a "Formulation 1", Post explica a identificação entre capacidade de resolver e seus formalismos adicionando algumas definições.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{description}
	\item[Aplicabilidade] ``Um conjunto de instruções é chamado aplicável a um problema genérico, se ao aplicá-lo a um caso específico do problema, a instrução (a) nunca é dada quando a célula em que a cabeça está já está marcada, e (b) nunca é dada quando a célula está desmarcada. Um conjunto de instruções aplicável a um problema genérico inicia um processo determinístico quando aplicado à cada problema específico. Esse processo termina quando e somente quando ele chega a uma instrução do tipo (C).''
\pause
	\item[Finite 1-Process] ``Um conjunto de instruções então será instruído para iniciar um finite 1-process em conexão com o problema genérico se aplicável ao problema e \textit{se o processo que determina terminar para cada problema específico}.''
	\end{description}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{description}
	\item[1-solution] ``Um finite 1-process associado à um problema genérico será tido como \textit{1-solution} de um problema se a resposta que ele dá a cada problema específico for correta''.
\pause
	\item[1-given] Um problema é 1-given se um finite 1-process pode ser configurado no qual, quando aplicado à classe dos números naturais, simbolizada de uma certa maneira no symbol space, entrega de maneira biunívoca a classe específica de problemas que constituem o problema genérico.
	\end{description}
\end{frame}

\begin{frame}
\frametitle{Máquina de Post}
	\begin{itemize}
	\item Baseado nos formalismos acima conseguimos montar a noção de resolvibilidade:
		\begin{center}
		Um problema é resolvível se for possível configurar um finite 1-process relativo ao problema (1-given) que é uma 1-solution.
		\end{center}
\pause
	\item O problema da divisibilidade falado anteriormente é, nesses termos, resolvível. No mesmo escopo o \textit{Entscheidungsproblem} é um problema 1-given para qual não há finite 1-process que seja 1-solution.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Entscheidungsproblem}
Apenas como curiosidade
	\begin{itemize}
	\item O \textit{Entscheidungsproblem} (termo alemão para "problema de decisão") é um problema de lógica que consiste em achar um algoritmo genérico que recebe como entrada a descrição de uma linguagem formal e um enunciado matemático na linguagem e produz como resposta "verdadeiro" ou "falso".
\pause
	\item Tanto Church como Turing mostraram que é impossível decidir algoritmicamente se um enunciado na aritmética é verdadeiro ou falso.
\pause
	\item A idéia do problema veio de Gottfried Leibniz que desejava construir uma máquina que pudesse manipular símbolos a fim de determinar os valores de verdade dos enunciados matemáticos.
\pause
	\item Turing reduziu o problema da parada para as máquinas de Turing ao \textit{Entscheidungsproblem} e provou que era impossível tal algoritmo.
	\end{itemize}
\end{frame}

% Post correspondence problem
\begin{frame}
\frametitle{Post correspondence problem}
	\begin{itemize}
	\item O problema de correspondência de Post é um exemplo de problemas indecidíveis. Foi apresentado por Post em 1946. Ele é mais simples que o problema da parada e que o \textit{Entscheidungsproblem}, por isso, é frequentemente usado para demonstrações de indecidibilidade.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Post correspondence problem}
	\begin{itemize}
	\item A entrada do problema consiste de duas listas finitas $u_1, ... ,u_n$ e $v_1, ... , v_n$ de palavras sobre um alfabeto A tendo pelo menos dois símbolos. Uma solução para esse problema é uma sequência de índices $(i_k)_{i\leq k\leq K}$ com $K \geq 1$ e $1 \leq i_k \leq K$ para todo $k$, onde\\
		\begin{center}
		{${u_i}_1 ... {u_i}_k = {v_i}_1 ... {v_i}_k$}
		\end{center}
	O problema de decisão é decidir se essa solução existe ou não.
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Post correspondence problem}
	\begin{itemize}
	\item Exemplo:\\
	Considere as seguintes listas\\
	\begin{center}
		\begin{tabular} {|c | c || c | c|}
		\hline
		$u_1$ & aba & $v_1$ & a \\ \hline
		$u_2$ & bbb & $v_2$ & aaa \\ \hline
		$u_3$ & aab & $v_3$ & abab \\ \hline
		$u_4$ & bb & $v_4$ & babba \\
		\hline
		\end{tabular}
	\end{center}
	\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Post correspondence problem}
\begin{center}
	\begin{tabular} {|c | c || c | c|}
	\hline
	$u_1$ & aba & $v_1$ & a \\ \hline
	$u_2$ & bbb & $v_2$ & aaa \\ \hline
	$u_3$ & aab & $v_3$ & abab \\ \hline
	$u_4$ & bb & $v_4$ & babba \\
	\hline
	\end{tabular}
\end{center}
A solução para o problema seria a sequência 1, 4, 3, 1, pois:
	\begin{center}
	$u_1u_4u_3u_1 = aba + bb + aab + aba = ababbaababa = a + babba + abab + a = v_1v_4v_3v_1$\\
	\end{center}
Entretanto, se as listas consistissem apenas de $u_1,u_2,u_3$ e $v_1,v_2,v_3$, então não haveria solução.
\end{frame}

\begin{frame}
\frametitle{Referências Bibliográficas}
	\begin{itemize}
	\item V.A. Uspensky - Post's Machine, 1983
	\item Liesbeth De Mol - Post's Machine
	\item http://en.wikipedia.org/wiki/Entscheidungsproblem
	\item http://en.wikipedia.org/wiki/Halting\_problem
	\item http://en.wikipedia.org/wiki/Formulation\_1
	\item http://www.gallois.com.br/tec/post\_machine
	\end{itemize}
\end{frame}

\end{document}