Algebraic combinatory models
share
We introduce an equationally definable counterpart of the notion of combinatory model. The new notion, called an algebraic combinatory model, is weaker than that of a lambda algebra but is strong enough to interpret lambda calculus. The class of algebraic combinatory models admits finite axiomatisation with seven closed equations, and it can be characterised as the retracts of combinatory models. Lambda algebras are then characterised as algebraic combinatory models which are stable, and there is a canonical construction of a lambda algebra from an algebraic combinatory model. This passage to a lambda algebra also manifests itself in our construction of a cartesian closed category with a reflexive object from an algebraic combinatory model. The resulting axiomatisation of lambda algebras with the seven equations and stability corresponds to that of Selinger [J. Funct. Programming, 12(6), 549-566, 2002], which would clarify the origin and the role of each axiom in his axiomatisation.
READ FULL TEXT