Partial combinatory algebra: Difference between revisions

Revision as of 13:29, 24 February 2025

Revision as of 17:32, 25 February 2025

Line 3:

==Definition==

A ''partial applicative structure''{{r|van-oosten|p=1}} is simply a set <math>A</math> equipped with a [[partial function|partial]] binary operation <math>A \times A \rightharpoonup A</math>. In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e., <math>(a, b) \mapsto a b</math>. It is usually ''not'' associative; by convention, the notation <math>a b c</math> associates to the left as <math>(a b) c</math>, matching the standard convention in [[λ-calculus]].

The ''terms''{{r|van-oosten|p=2}} (or ''expressions'') over a partial applicative structure <math>A</math> are defined inductively:

* A constant <math>a \in A</math> is an expression,

Line 15:

A term is ''closed'' if it contains no variables. A closed term may be ''evaluated'' in the natural way: a constant <math>a \in A</math> evaluates to itself, and if the terms <math>e_1</math> and <math>e_2</math> respectively evaluate to <math>a_1</math> and <math>a_2</math>, then <math>e_1 e_2</math> evaluates to <math>a_1 a_2</math>, if this is defined. Note that the evaluation is a partial operation, since not all applications are defined. A substitution operation is also defined in the natural way: if <math>t</math> is a term, <math>x</math> is a variable and <math>u</math> is another term, <math>t[u/x]</math> denotes the term <math>t</math> with all occurrences of <math>x</math> replaced by <math>u</math>. We write <math>t \downarrow</math> to simultaneously express that the term <math>t</math> evaluates to a defined value and denote this value (this matches standard notation for values of [[partial functions]]). We also write <math>t \simeq u</math> when both closed terms <math>t</math> either do not evaluate to a defined value, or evaluate to the same value.

The partial applicative structure ''A'' is said to be ''combinatory complete''{{r|van-oosten|p=3}} or ''functionally complete'' if, for every term <math>t(x_0, \dots, x_n)</math> (that is, a term <math>t</math> whose variables are among <math>x_0, \dots, x_n</math>), there exists an element <math>a \in A</math> such that:

* <math>a a_0 \dots a_{n-1} \downarrow</math> for all <math>a_0, \dots, a_{n-1} \in A</math>,

* <math>a a_0 \dots a_n \simeq t[a_0/x_0, \dots, a_n/x_n]</math> for all <math>a_0, \dots, a_n \in A</math>.

A '''partial combinatory algebra'''{{r|van-oosten|p=3}} (pca) is a combinatory complete partial applicative structure. A '''total combinatory algebra''' (tca) is a pca whose application operation is total.

Informally, the combinatory completeness condition requires an analogue of the abstraction operation from lambda calculus to exist inside the pca.

Line 28:

In the same way as there is a translation from [[λ-term]]s to terms of the [[SKI combinator calculus]] by eliminating [[λ-abstraction]]s using combinators, pcas can be characterized by the existence of elements which satisfy equations analogous to the S and K combinators. Note, however, that some care must be taken in the statement and proof since application is not always defined in a pca.

'''Theorem:'''{{r|van-oosten|p=3}} A partial applicative structure <math>A</math> is combinatory complete if and only if there exist two elements <math>k, s \in A</math> such that:

* <math>K x y \downarrow = x</math> for all <math>x, y \in A</math>,

Line 63:

We can form a pca (in fact a tca) by quotienting the set of closed (untyped) λ-terms by [[β-equivalence]] and taking the application to be the one inherited from λ-calculus.

==NotesReferences==

<references>

<ref name=van-oosten>{{ cite book | title = Realizability: an introduction to its categorical side | author = Jaap van Oosten | isbn = 9780444515841 | year = 2008 | publisher = Elsevier Science | pages = 328 }}</ref>

</references>

{{refbegin}}

* <ref name=van-oosten>{{ cite book | title = Realizability: an introduction to its categorical side | author = Jaap van Oosten | isbn = 9780444515841 | year = 2008 | publisher = Elsevier Science | pages = 328 }}</ref>

{{refend}}

{{mathlogic-stub}}