Popis: |
In the previous chapter, broadly speaking, we axiomatized and studied higher-order models as combinatory algebras—that is, as structures possessing elements k and s satisfying certain axioms. In the present chapter, we shall consider models from the related but somewhat different perspective of the λ-calculus. Not all the models mentioned in Chapter 3 satisfy the fundamental rules of the λ-calculus, but for those that do—the so-called typed λ-algebras—a wealth of further structure is available, and our purpose here is to study this structure in a general setting. |