External and internal syntax of the λ-calculus

摘要

It is well known that formally defining and reasoning about languages with binding (such as logics and λ-calculii) is problematic. There are many approaches to deal with the problem, with much work over recent years stimulated by the desire to formally reason about programming languages and program logics. The various approaches have their own strengths and drawbacks, but no fully satisfactory approach has appeared.rnWe present an approach based on two levels of syntax: an internal syntax which is convenient for machine manipulation, and an external syntax which is the usual informal syntax used in many articles and textbooks. Throughout the paper we use pure λ-calculus as an example, but the technique extends to many languages with binding.rnOur internal syntax is canonical: one representative of every α-equivalence class. It is formalized in Isabelle/HOL, and its properties are mechanically proved. It is also proved to be isomorphic with a nominal representation of λ-calculus in Isabelle/HOL.rnOur conventional, human friendly external syntax is naturally related to the internal syntax by a semantic function. We do not define notions directly on the external syntax, since that would require the usual care about α-renaming, but introduce them indirectly from the canonical internal syntax via the semantic function.