Objetivos Gerais:

1 - Estudo dos limites da computação.
2 - Prática de programação com "go to's" e definição de funções.
3 - Conhecer os fundamentos lógicos e algébricos de alguns dos paradigmas da programação já estudados pelos alunos (imperativo; recursivo; e reescrita e utilização de tipos abstratos).

Conteúdos / Programa:

1 - Teoria da Computabilidade.
1.1 - Máquina de registos URM e funções URM-computáveis.
1.2 - Geração de funções URM-computáveis; funções recursivas primitivas e funções parciais recursivas.
1.3 - Máquina de Turing e funções Turing-computáveis, e referência a outras abordagens à computabilidade. Tese de Church.
1.4 - Codificação dos programas URM. O método da diagonal e demonstração de que existem funções não computáveis. O teorema s-m-n.
1.5 - Programas universais. Decidibilidade, total e parcial, e indecidibilidade.
2 - Fundamentos Lógicos e Algébricos da Computação.
2.1 - Cálculo de Hoare e prova da correção (parcial) de programas imperativos.
2.2 - Definição de funções por recursão. Prova da correção de programas recursivos utilizando o princípio de indução (bem fundada).
2.3 - Especificações equacionais de tipos de dados abstratos. Linguagem. Cálculo equacional. Reescrita.

Bibliografia / Fontes de Informação:

A.G. Hamilton , 1988 , Logic for Mathematicians , Cambridge University Press
Carmo, J., Gouveia, P e Dionísio, F. , 2013 , Elementos de Matemática Discreta , College Publications
N.J. Cutland , 1980 , Computability - An Introduction to Recursive Function Theory , Cambridge Press
A. Sernadas & C. Sernadas , 1999 , Fundamentos Algébricos da Engenharia da Programação , Instituto Superior Técnico
G. Boolos e R. Jeffrey , 1990 , Computability and Logic , Cambridge University Press
D. Bridges , 1994 , Computability: A Mathematical Sketchbook , Springer-Verlag
B.F. Chellas , 1980 , Modal Logic: An Introduction , Cambridge University Press
F. Coelho e J.P. Neto , 2010 , Teoria da Computação - Computabilidade e Complexidade , Escolar Editora
M. Davis , 1983 , Computability and Unsolvability , Dover
M. Davis e E. Weyuker , 1983 , Computability, Complexity and Languages , Academic Press
P. Dume , 1991 , Computability Theory: Concepts and Applications , Ellis Horwood
H. Ehrig e B. Mahr , 1985 , Fundamentals of Algebraic Specification I , Springer Verlag
R.L. Epstein e W.A. Carnielli , 1999 , Computability: computable functions, logic and the foundations of mathematics , Wadsworth
R. Goldblat , 1982 , Axiomatising the Logic of Computer Programming , Springer
R. Goldblat , 1992 , Logics of Time and Computation , CSLI
V.J. Rayward-Smith , 1995 , A First Course in Computability , McGraw-Hill (computer Science Texts)
C. Sernadas , 1993 , Introdução à Teoria da Computação , Editorial Presença
A. Sernadas e C. Sernadas , 2012 , Fundamentos de Lógica e Teoria da Computação , College Publications

Métodos e Critérios de Avaliação:

Tipo de Classificação: Quantitativa (0-20)

Metodologia de Avaliação:
Aulas teóricas expositivas, procurando ilustrar os conceitos através de vários exemplos. Aulas teórico-práticas de resolução de problemas. A avaliação é feita através de duas frequências, cada uma com um peso de 50% na classificação final.