λ-sub as an explicit substitution calculus
September 2006
Abstract
This work explores confluence and termination in Milner's encoding of the λ-calculus as a bigraphical reactive system. In that work, the λ-calculus was extended with explicit subsitutions and the extension (λsub) was encoded as a bigraphical reactive system.
We prove that the reduction relation of the extension is confluent on ground terms and preserves strong normalisation (PSN) of β-reduction. This gives us corresponding proofs for the bigraphical encoding. The proofs are based on the strong relationship between λsub and the calculus λxgc of Bloo and Rose. The notion of composition of substitutions in λsub and the problems it raises when attempting to prove PSN are discussed.
We then exploit similarities between λsub and the λlxr calculus of Kesner and Lengrand to present a translation from λsub to a modified version of λlxr. We show that reduction in the former may be simulated in the latter which leads to a clearer proof of PSN for λsub.
Technical report TR-2006-95 in IT University Technical Report Series, September 2006.
Available as PostScript, and PDF.