Title Confluence of untyped lambda calculus via simple types
Authors Silvia Ghilezan, Computing Science Department, Catholic University
Viktor Kuncak, Laboratory of Computer Science, MIT
Main Fields 21. type theory
Other Main Fields lambda calculus
Abstract + Keywords We present a new proof of confluence of the untyped lambda calculus by embedding untyped lambda terms
into simply typed lambda terms. This embedding allows us to define a reduction on all lambda terms, whose
transitive closure is the beta reduction, using an auxiliary reduction and the beta reduction on simply typed
lambda terms. The confluence of the auxiliary reduction makes explicit the joining of the sets of redexes to be 
reduced. This embedding allows us to use the confluence of beta reduction on simply typed lambda terms and
thus prove the confluence of the reduction defined. As a consequence we obtain the confluence of beta reduction 
in theuntyped lambda calculus.