Teoria da Computação
(cod.5384)

1  Novidades

• Uma versão actualizada desta página encontra-se localizada na página e-conteudos
• Novo turno Prático: Quinta-Feira das 14h00 às 16h00 na sala 6.14.

Contents

• 1  Novidades
• 2  Docentes
• 3  Objectivos
• 4  Programa
• 5  Critérios de Avaliação
  • 5.1  Componente Ensino/Aprendizagem
  • 5.2  Admissão e Avaliação por Exame
• 6  Datas Importantes
• 7  Material Pedagógico
• 8  Horário
• 9  Atendimento
• 10  Alunos de Engenharia Informática inscritos
• 11  Bibliografia Principal
• 12  Links úteis

2  Docentes

3  Objectivos

1. perceber a capacidade de computação das máquinas, assim como os seus limites teóricos. Precisaremos de definir formalmente o que é e o que não é um programa, um algoritmo, ou mais genericamente o que é um tratamento efectivo;
2. perceber os conceitos que fundamentam as linguagens de programação. Precisaremos de determinar e estudar formalmente as construções que determinam a expressividade (ou capacidade de computação) das linguagens de programação assim como o comportamento dos programas.

4  Programa

• Apresentação Contextual e Histórica da Teoria da computação
• Modelos da computação: dos autómatos (de estados finitos, com pilha) às máquinas de Turing.
• Modelos de computação alternativos: Funções recursivas de Kleene e calculo lambda.
• Programação em modelos da computação.
• Tese de Church-Turing. Provas de equivalência de modelos.
• A não computabilidade e a indecidibilidade: Problemas indecidíveis, técnica da diagonalização, técnica da redução.
• Complexidade. Introdução: problemas tratáveis e problemas intratáveis. Critérios de catalogação (memória, tempo, etc.). Caracterização das classes NP, P e NP-Completo. Problemas NP-Completos: Exemplos. Técnica da redução polinomial para a demonstração de NP-completude.
• Análise de complexidade: analíse assimptótica, no pior dos casos, e em média.

5  Critérios de Avaliação

5.1  Componente Ensino/Aprendizagem

• A avaliação contínua mede em termos práticos a acquisição dos conceitos expostos. Como tal é baseada na avaliação da resolução de exercícios durante as práticas laboratóriais.
• Os exercicios avaliados são em número de 8. Os enunciados serão sempre entregue na semana anterior a sua resolução.
• A Nota da Componente Prática (NCP, 20 valores) a soma dos valores atribuidos aos diferentes exercícios resolvidos.

5.2  Admissão e Avaliação por Exame

• Mínimos: é admitido a exame quem tiver a nota NCP≥ 7. Isto é: qualquer nota NCP maior ou igual a 7 significa admissão ao exame.
• A prova escrita do exame dará lugar a Nota da Prova Escrita (NPE, 20 valores). Esta nota carece do mesmo mínimo do que a avaliação contínua: tem de ser maior ou igual a 7 para possibilitar a aprovação à disciplina.
• Assim a nota final (NFin) é calculada da seguinte forma:

  NFin=if (NPE≥ 7 ∧ NPC≥ 7) then

  NPE*12 + NCP*8 20

  else Reprovado

6  Datas Importantes

• Exame Época 1 : (por confirmar)
• Exame Época 2 : (por confirmar)
• Exame Época Especial : (por confirmar)

7  Material Pedagógico

Fichas práticas

8  Horário

9  Atendimento

10  Alunos de Engenharia Informática inscritos

11  Bibliografia Principal

12  Links úteis

• Ocaml
  • Site OCaml
  • Performance Ocaml:The great computer language shootout
  • OCamlMakefile: Makefile genérico para OCaml
  • Tuareg: Emacs Mode para Ocaml
  • Livro: Developing Applications With Objective Caml
  • Manual de Referência Ocaml
  • Sebentas diversas sobre Ocaml
  • Hump: Repositório de aplicações/bibliotecas/”material” OCaml
  • Documentação adicional (em françês)
• COQ
  • Página Principal do Sistema COQ
  • ProofGeneral: um Emacs Mode para COQ
  • Livro: COQ'ART: Interactive Theorem Proving and Program Development
  • Manual de Referência COQ
  • Tutorial COQ
  • Bibliotecas COQ
  • Tutorial sobre Tipos recursivos em COQ
  • CoqIDE, um IDE para COQ.
• Emacs
  • Site Emacs - XEmacs
  • Documentação Emacs - XEmacs
  • Comandos principais para Emacs 21
• Um site sobre Ciências da Computação (contem livros online)
  • Site Programming languages theory texts online

References

[1]

Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C.7, pages 739–782. North-Holland, Amsterdam, 1977.

[2]

A. Arnold and I. Guessarian. Mathematics for Computer Science. Prentice-Hall, 1996.

[3]

F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[4]

D. Bagley. The great computer language shootout. http://www.bagley.org/~doug/shootout

[5]

H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.

[6]

H.P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–310. Oxford University Press, New York, 1992.

[7]

S. Burris and H. Sankappanavar. A Course in Universal Algebra. Springer Verlag, 1981. http://www.cs.uu.nl/people/franka/ref

[8]

E. Chailloux, P. Manoury, and B. Pagano. Developing applications with objective caml. http://caml.inria.fr/oreilly-book, 2003.

[9]

T. Coquand and P. Dybjer. Inductive definitions and type theory: an introduction. In Foundations of Software Technology and Theoretical Computer Science, pages 60–76, 1994. http://www.math.chalmers.se/~peterd/papers/ESSLLI94.ps.gz

[10]

R. Cori and D. Lascar. Mathematical Logic : A course with exercises – Part I. Oxford University Press, 2000.

[11]

R. Cori and D. Lascar. Mathematical Logic : A course with exercises – Part II. Oxford University Press, 2001.

[12]

G. Cousineau and M. Mauny. The functional approach to programming. Cambridge University Press, 1998.

[13]

N. J. Cutland. Computability. Cambridge University Press, 1980.

[14]

B. A. Davey and H. A. Priestley. Introduction to Lattices and Order: Second Edition. Cambridge University Press, 2002.

[15]

G. Dowek. La logique. Coll. Dominos. Flammarion, 1995.

[16]

G. Dowek. Le langage mathématique et les langages de programmation. Voir, entendre, raisonner, calculer. Cité des sciences et de l'industrie, La Villette, Paris, 1997. http://www.lix.polytechnique.fr/~dowek/Vulg/langagelangages.ps.gz

[17]

G. Dowek. Higher-order unification and matching. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 16, pages 1009–1062. Elsevier Science Publishers B.V., 2001.

[18]

G. Dowek. Théories des types. DEA Programmation, Paris VII, 2002. http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz

[19]

P. Fejer and D. Simovici. Mathematical Foundations of Computer Science, Volume 1: Sets, Relations and Induction,. Texts and Monographs in Computer Science. Springer Verlag, 1991.

[20]

E. Gimenez. A tutorial on recursive types in Coq. http://coq.inria.fr/doc-eng.html

[21]

J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988.

[22]

C. Hall and J. O'Donnell. Discrete Mathematics Using A Computer. Springer Verlag, 2000.

[23]

Chris Hankin. Lambda Calculi: A Guide for Computer Scientists, volume 3 of Graduate Texts in Computer Science. Clarendon Press, Oxford, 1994.

[24]

D. R. Hofstadter. Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books, New York, 1979.

[25]

G. Huet. Constructive computation theory. Course Notes, DEA Informatique Université Bordeaux I, October 1992. http://pauillac.inria.fr/~huet/CCT/

[26]

N. D. Jones. Computability and Complexity from a Programming Perspective. Foundations of Computing. MIT Press, Boston, London, 1 edition, 1997.

[27]

J. W. Klop. Term rewriting systems. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, New York, 1992.

[28]

W. Kneale and M. Kneale. O Desenvolvimento da Lógica. Fundação Calouste Gulbenkian, (1962) - 1991. Terceira Edição.

[29]

J. L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood, 1993.

[30]

P. Linz. An introduction to formal languages and automata. Jones and Bartlett Publisher, 2006.

[31]

H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons, Chichester, 1993. http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

[32]

L. Pequet. Programmation fonctionelle - introduction illustrée en objective caml. http://www-rocq.inria.fr/~pecquet/pro/teach/teach.html, 2002.

[33]

A. Pitts. Lecture notes on denotational semantics. University of Cambridge Computer Laboratory, 1999. http://www.cl.cam.ac.uk/Teaching/1998/DenoSema/dens.ps.gz

[34]

A. Pitts. Lecture notes on computation theory. University of Cambridge Computer Laboratory, 2002. http://www.cl.cam.ac.uk/Teaching/2002/CompTheory

[35]

F. Prost and G. Kahn. Checking mathematical facts with coq: Various examples of Coq proofs. http://coq.inria.fr/contribs-eng.html

[36]

Didier Rémy. Using, Understanding, and Unraveling the OCaml Language. In Gilles Barthe, editor, Applied Semantics. Advanced Lectures. LNCS 2395., pages 413–537. Springer Verlag, 2002. http://pauillac.inria.fr/~remy/cours/appsem/ocaml.pdf

[37]

M. Sipser. Introducton to the Theory of Computation. PWS Publishing, 2006.

[38]

Coq Development Team. Documentation of the coq theorem prover. http://coq.inria.fr/doc-eng.html

[39]

Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[40]

Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[41]

OCaml Development Team. The Objective Caml system:Documentation and user's manual, 2002. http://caml.inria.fr/ocaml/htmlman/index.html

[42]

Isabelle Tellier. Introduction à l'informatique. http://www.grappa.univ-lille3.fr/polys/intro-info/index.html, 2001.

[43]

D. van Dalen. Logic and Structure. Springer Verlag, Berlin, Germany, 1983.

[44]

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge, Massachusetts, February 1993.

[45]

Bertot Y and P. Castéran. Coq'art. http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html, 2003.

This document was translated from L^AT_EX by H^EV^EA.