Substitution Theorem Seminars/Workshops

Abstract

This talk proved two theorems: Substitution theorem and characterization of persistently strongly normalizing terms. Substitution theorem is for usual lambda calculus (untyped lambda calculus with beta-reduction). We say a term M is strongly normalizing if it terminates with any reduction strategy. A simple instance of Substitution theorem is that for any term M, MXYZ is strongly normalizing for any strongly normalizing terms X, Y, Z if MXXX is strongly normalizing for any strongly normalizing term X. This means that in order to prove termination of a 3-place function f(x,y,z) in a functional programming language, it is sufficient to show termination of the function call f(x,x,x). A term M is called persistently strongly normalizing if MX_1 ... X_n is strongly normalizing for any n and any strongly normalizing terms X_1, ... X_n. A type theoretic characterization of these terms was a long-standing open question. This talk solved this problem by using Substitution theorem. This is a joint work with Mariangiola Dezani-Ciancaglini (Torino University).