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 they are shown to be exactly the retracts of combinatory models. Lambda algebras are then characterised as algebraic combinatory models which are stable; moreover there is a canonical construction of a lambda algebra from an algebraic combinatory model. The resulting axiomatisation of lambda algebras with the seven equations and the axiom of 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.
翻译：我们引入了可等式分解的组合模型概念对应方。 被称为代数组合模型的新概念比羊羔代数模型弱,但足够强,足以解释羊羔计算。 代数组合模型的等级承认有7个封闭方程式的有限分解, 并显示它们正是复式模型的缩影。 Lambda代数随后被定性为稳定的代数组合模型; 此外,一个代数组合模型的羊驼代数模型的粗体构造。 由此形成的羊驼代数与7个方程式和稳定性的轴对应于Selinger[J. Funct. 编程, 12(6), 549-566, 2002], 它将澄清每种氧化物的起源和作用。
相关内容
微信扫码咨询专知VIP会员