Monadic presentations of lambda terms using generalized inductive types
T Altenkirch, B Reus - … Science Logic: 13th International Workshop, CSL'99 …, 1999 - Springer
Computer Science Logic: 13th International Workshop, CSL'99 8th Annual …, 1999•Springer
We present a definition of untyped λ-terms using a heterogeneous datatype, ie an
inductively defined operator. This operator can be extended to a Kleisli triple, which is a
concise way to verify the substitution laws for λ-calculus. We also observe that repetitions in
the definition of the monad as well as in the proofs can be avoided by using well-founded
recursion and induction instead of structural induction. We extend the construction to the
simply typed λ-calculus using dependent types, and show that this is an instance of a …
inductively defined operator. This operator can be extended to a Kleisli triple, which is a
concise way to verify the substitution laws for λ-calculus. We also observe that repetitions in
the definition of the monad as well as in the proofs can be avoided by using well-founded
recursion and induction instead of structural induction. We extend the construction to the
simply typed λ-calculus using dependent types, and show that this is an instance of a …
Abstract
We present a definition of untyped λ-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended to a Kleisli triple, which is a concise way to verify the substitution laws for λ-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed λ-calculus using dependent types, and show that this is an instance of a generalization of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.
Springer