Reseña: Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus

Se ha publicado un artículo de razonamiento formalizado en Agda sobre metalógica titulado Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus.

Sus autores son Álvaro Tasistro, Ernesto Copello y Nora Szasz (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).

Su resumen es

In Substitution revisited, Alley Stoughton proposed a notion of (simultaneous) substitution for the Lambda calculus as formulated in its original syntax – i.e. with only one sort of symbols (names) for variables – and without identifying α-convertible terms. According to such formulation, the action of substitution on terms is defined by simple structural recursion and an interesting theory arises concerning the connection to α-conversion.

In this paper we present a formalisation of Stoughton’s work in Constructive Type Theory using the language Agda, which reaches up to the Substitution Lemma for α-conversion. The development has been quite inexpensive e.g. in labour cost, and we are able to formulate some improvements over the original presentation. For instance, our definition of α-conversion is just syntax directed and we prove it to be an equivalence relation in an easy way, whereas in Substitution revisited the latter was included as part of the definition and then proven to be equivalent to an only nearly structural definition as corollary of a lengthier development. As a result of this work we are inclined to assert that Stoughton’s is the right way to formulate the Lambda calculus in its original, conventional syntax and that it is a formulation amenable to fully formal treatment.

El trabajo se ha publicado en Electronic Notes in Theoretical Computer Science.

El código de las correspondientes teorías en Agda literario se encuentra aquí.