We introduce the notion of ref lexivity for combinatory algebras. Ref lexivity can be thought of as an equational counterpart of the Meyer–Scott axiom of combinatory models, which indeed allows us to characterize an equationally definable counterpart of combinatory models. This new structure, called strongly reflexive combinatory algebra, admits a finite axiomatization with seven closed equations, and the structure is shown to be exactly the retract of combinatory models. Lambda algebras can be characterized as strongly ref lexive combinatory algebras that are stable. Moreover, there is a canonical construction of a lambda algebra from a strongly ref lexive combinatory algebra. The resulting axiomatization of lambda algebras by the seven axioms for strong ref lexivity together with those for stability is shown to correspond to the axiomatization of lambda algebras due to Selinger (2002, J. Funct. Program., 12, 549–566).
展开▼
