Partial combinatory algebra: Difference between revisions

Revision as of 17:12, 21 February 2025

Revision as of 17:13, 21 February 2025

Line 34:

* <math>S x y z \simeq (x z) (y z)</math> for all <math>x, y, z \in A</math>.

For the proof, in the forward direction, if <math>A</math> is combinatory complete, it suffices to apply the definition of combinatorialcombinatory completeness to the terms <math>t_K(x, y) := x</math> and <math>t_S(x, y, z) := (x z)(y z)</math> to obtain <math>K</math> and <math>S</math> with the required properties.

It is the converse that involves abstraction elimination. Assume we have <math>K</math> and <math>S</math> as stated. Given a variable <math>x</math> and a term <math>t</math>, we define a term <math>\langle x \rangle t</math> whose variables are those of <math>t</math> minus <math>x</math>, which plays a role similar to <math>\lambda x \cdot t</math> in λ-calculus. The definition is by induction on <math>t</math> as follows: