%\documentclass[dvips,12pt]{amsart}
\documentclass[pdftex,12pt]{amsart}
\usepackage{amssymb}
\usepackage[portuges]{babel}
\usepackage{color}
\usepackage{epsfig}

\title{Teoria da Computa\c c\~ao\\
       Satisfaction}

\author{Raul H.C.Lopes}

\usepackage{listings}
\input{deflogic}
\input{defseqs}
\input{defport}
%\input{defproglangs}
%\input{defenvs}

\input{defcomputability}
\input{defcomplexity}
\def\beq{\begin{equation}}
\def\eeq{\end{equation}}
\def\SC{\textbf{Senhor do Castelo}}

\def\marker{\emph{marker}}




\begin{document}
\maketitle
\section{Introdu\c c\~ao}
Esta lista deve ser resolvida individualmente. Entregue suas respostas em folha
de papel decente, preenchida a caneta.

\section{Nota\c c\~ao axiomas}
A nota\cao\ de pontos de Curry, apresentada em sala e notas de aula
e  p\aa gina 34 de \cite{curry:foundations}, \ee\ utilizada para reduzir 
o uso de par\^enteses.
 
Uma \sqn\ de elementos de um tipo $A$  \ee\ uma \sqn\ vazia (denotada por
$\xnil$) ou resultado de adicionar um elemento de $A$ a uma \sqn\ de 
elementos de $A$. Os axiomas a seguir definem \sqn s de elementos
de $A$, denotada \sqntype A:
\begin{align}
	\label{nilseq} &\xnil \in \sqntype A\\
	\label{consseq} &(\xcons ax)\in\sqntype A \lif x\in\sqntype A \land a\in A\\
	\label{closure}& \text{fecho universal.}
\end{align}

Assumindo que $x,y\in\sqntype A$ e que $a,b\in A$, os seguintes axiomas 
tratam a igualdade sobre \sqn s.
\begin{align}
	\label{xnildif}&\xnil\neq (\xcons ax)\\
	\label{conseq} &(\xcons ax) = (\xcons by) \llr.= a=b \land x=y
\end{align}

O princ\ii pio da indu\cao\ sobre \sqn s estabelece condi\coes\ para que uma
propriedade $P$ seja v\aa lida para qualquer \sqn, sendo denotado
$WPI(P)$. 
\begin{align}
	WPS(P)&\dfn (\bndA{x}{x\in\sqntype A}{\bndA{a}{a\in  A}
                      {P.x}\limp P.\xcons ax})\\
		      WPI(P)&\dfn (P.\xnil\land WPS(P))\limp(\bndA{x}{x\in\sqntype
		      A}{P.x})
\end{align}
						      
As equa\coes\ a seguir definem o operador \emph{snoc} (denotado
\xsnocftor, em oposi\cao, logicamente ao operador \emph{cons}, \xconsftor).
\begin{align}
	\label{xnilsnoc}&\xsnoc \xnil a \llr.= \xcons a\xnil\\
	\label{xconsnoc}&\xsnoc{(\xcons ax)}b \llr.= \xcons a{(\xsnoc xb)}
\end{align}
As equa\coes\ a seguir definem um operador \emph{cat} (denotado \xcatftor) para
concatenar duas \sqn s.

\begin{align}
	\label{xnilxcat} &\xcat\xnil y = y\\
	\label{xconsxcat} & \xcat{(\xcons ax)}y =. \xcons a{(\xcat xy)}
\end{align}

Pertin\^encia em uma \sqn\ \ee\ definida a seguir.
\begin{align}
	\label{xnilin}&a\not\in\xnil\\
	\label{xconsin}& a\in (\xcons bx) =\lr. a=b\lor a\in x\\
\end{align}

O n\uu mero de elemtos de uma \sqn\ \ee\ definido a seguir:
\begin{align}
	\label{xnilen}\sqnlen \xnil = 0\\
	\label{xconslen}\sqnlen{\xcons ax} = 1+\sqnlen x
\end{align}

\section{Seq\"u\^encias}
\begin{qst}
	Seja $R$ uma propriedade sobre \sqn s e sejam
	\begin{align*}
	SPS(R)& \dfn\ \bndA{x,y}{x,y\in\sqntype A\land \sqnlen y<\sqnlen x}{R.y\limp R.x}\\
	SPI(R)&\dfn\ (R.\xnil\land SPS(R))\limp 
	               \bndA{x}{x\in\sqntype A}{R.x}
	\end{align*}

	Prove que 
	$$WPI(R)\limp SPI(R)$$
\solbeg
\textsl{DICAS:}
\begin{itemize}
	\item Note que $WPI(R)$ \ee\ apenas o princ\ii pio da indu\cao;
	\item A quest\ao\ demanda, portanto provar $SPI(R)$ por indu\cao;
	\item Isso consiste em assumir $SPS(R)$ e provar 
		$\bndA{x}{x\in\sqntype A}{R(x)}$
		por indu\cao.
\end{itemize}

A prova \ee\ banal.
\solend
	
\end{qst}

\begin{qst}\label{merge}
	Defina uma fun\cao\ recursiva sobre \sqn s que, dadas duas \sqn s $x$ 
	e $y$, ordenadas,
	produz uma \sqn\ ordenada, cujos elementos s\ao\ exatamente os 
	elementos de \xcat xy. Prove sua corre\cao.
\end{qst}

\begin{qst}
	Use a fun\cao\ definida na quest\ao\ \ref{merge} e construa uma fun\cao\
	para ordenar \sqn s. Prove sua corre\cao.
\end{qst}

\section{Computabilidade}

\begin{qst}
	Apresente um algoritmo para encontrar o menor circuito de Hamilton de
	um grafo de $n$ v\ee rtices, assumindo que:
	\begin{itemize}
		\item $w_ij$ cont\ee m o peso da aresta $(i,j)$.
		\item $c_{Sj}$ 
			representa o menor caminho que sai v\ee rtice $1$,
			passa por todos os v\ee rtices de $S$ e chega a $j$.
		\item seu algoritmo usa programa\cao\ din\^amica, computado
			os $c_{Sj}$ para conjuntos de v\ee rtices $S$
			progressivamente maiores.
	\end{itemize}

	Qual a complexidade do seu algoritmo?

	\solbeg 
	\textsl{DISCAS:} 
	\begin{itemize}
		\item Assuma a exist\^encia de um algoritmo para calcular
			$c_{Sj}$, e ache o menor circuito hamiltoniano.
		\item Encontre algoritmo par $c_{Sj}$.
	\end{itemize}
	\solend
\end{qst}

\begin{qst}
	Apresente uma m\aa quina de Turing que decide o conjunto dos 
	pal\ii ndromos.
\end{qst}

\begin{qst}
	Prove que se uma linguagem $L$ \ee\ decid\ii vel em \bgo{f(n)} por
	uma \ndtm, ent\ao\ $L$ \ee\ decid\ii vel por \tm\ em \bgo{c^{f(n)}},
	para alguma constante $c$.
\end{qst}

\begin{qst}
	Sejam
	\begin{align*}
		L\subseteq\{x:x\in\Sigma^\ast\}\\
		\overset{-}{L}\subseteq\{x\in \Sigma^\ast:x\not\in L\}
	\end{align*}

	Prove que $L$ \ee\ recursiva se e somente se $L$ e $\overset -L$ 
	s\ao\ recursivamente
	enumer\aa veis.
\end{qst}

\begin{qst}
	Prove que $L$ \ee\ recursiva, ent\ao\ $\overset -L$ tamb\ee m \ee.
\end{qst}

\section{They think it's all over\ldots}

\begin{verse}
There's a sign on the wall\\
But she wants to be sure\\
'Cause you know sometimes words have two meanings.\\
In a tree by the brook\\
There's a songbird who sings,\\
Sometimes all of our thoughts are misgiven.
\end{verse}

\begin{flushright}\emph{Stairway to heaven,} Led Zeppelin\end{flushright}


\bibliography{abbrev,analysis,formal,maths,algorithms,program,string}


\bibliographystyle{amsplain}


 
\end{document}


 

