Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702): Difference between revisions

When he formulated the lambda calculus \textit{A. Church} [Ann. Math. (2) 33, 346--366 (1932; Zbl 0004.14507; JFM 58.0997.06)] left substitution, which is essential for \(\alpha\)- and \(\beta\)-reduction, undefined. \textit{H. B. Curry} and \textit{R. Feys} [Combinatory logic. Amsterdam: North-Holland Publishing Company (1958; Zbl 0081.24104)] did define this, but the substitution \((\lambda x.M)[y:=P]\), in the case where \(y\) is free in \(M\) and \(x\) is free in \(P\), is complex. One way around, this is to have separate sorts of free and bound variables. The authors develop a new meta theory, for the \(\lambda\)-calculus, in constructive type theory, where, as for Church and Curry, only one sort of names of variables is used. In order to overcome the complexity of substitution, they define, inductively, notions such as \(x\) is free in \(M\), \(x\) is fresh in \(M\) and a variant of the substitution first defined by \textit{A. Stoughton} [Theor. Comput. Sci. 59, No. 3, 317--325 (1988; Zbl 0651.03008)]. New formulations of \(\alpha\)- and \(\beta\)-reduction are given. Importantly, the identification of \(\alpha\)-equal terms is not needed. All the usual properties such as Church-Rosser and subject reduction are proved using detailed but elementary proofs. They have machine checked the whole development using the system Agda.