9 - Correspondence between λ and CL

Summary

Introduction

Everything done so far has emphasized the close correspondence between λ and CL, in both motivation and results, but only now do we have the tools to describe this correspondence precisely. This is the aim of the present chapter.

The correspondence between the ‘extensional’ equalities will be described first, in Section 9B.

The non-extensional equalities are less straightforward. We have =_β in λ-calculus and =_w in combinatory logic, and despite their many parallel properties, these differ crucially in that rule (ξ) is admissible in the theory λβ but not in CL_w. To get a close correspondence, we must define a new relation in CL to be like β-equality, and a new relation in λ to be like weak equality. The former will be done in Section 9D below. (An account of the latter can be found in [ç H98].)

Notation 9.1 This chapter is about both λ- and CL-terms, so ‘term’ will never be used without ‘λ-’ or ‘CL-’.

For λ-terms we shall ignore changes of bound variables, and ‘M ≡_αN’ will be written as ‘M ≡ N’. (So, in effect, the word ‘λ-term’ will mean ‘α-convertibility class of λ-terms’, i.e. the class of all λ-terms α- convertible to a given one.)

Define

• ∧ = the class of all (α-convertibility classes of) λ-terms,

• C = the class of all CL-terms.