Substitution Theorem Seminars/Workshops
|Speaker:||Prof. Makoto Tatsuta|
|Place:||Room 319-1, Bldg 302, SNU|
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).
[ List ]