Bruno Dinis
CMAF-CIO, Universidade de Lisboa
Abstract:
In this talk we present a new method for proving strong normalization for higher type rewrite systems, due to Ulrich Berger [1], which makes use of a strict continuous domain-theoretic semantics. In order to understand Berger's method we start by showing, using essentially William Tait's method of strong computability [4], that a $\lambda$-calculus formulation of Gödel's T is strongly normalizing. The fact that Gödel's T is strongly normalizing is well-known and extensively studied in the literature.
We give a brief introduction to Clifford Spector's bar recursion [3] and to some domain-theoretic notions and tools necessary to carry out the proof that Gödel's T extended with bar recursors is also strongly normalizing. Finally, we will discuss the possibility of adapting Berger's method to show a strong normalization theorem for an extension with bar recursors of a theory of Fernando Ferreira and Gilda Ferreira, presented in [2].
[1] U. Berger, Continuous Semantics for Strong Normalization. In S. B. Cooper, B. Löwe and L. Torenvliet, editors, New Computational Paradigms: First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, Springer Berlin Heidelberg, pp.23-34 (2005).
[2] F. Ferreira and G. Ferreira, A herbrandized functional interpretation of classical first-order logic (manuscript).
[3] C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics. 5. American Mathematical Society. pp. 1-27 (1962).
[4] W. Tait, Normal form theorem for barrecursive functions of finite type. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pp. 353-367. North-Holland, Amsterdam (1971).
This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.
