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. |