Partial combinatory algebra: Difference between revisions

Revision as of 17:29, 21 February 2025

Latest revision as of 19:07, 18 March 2025

(19 intermediate revisions by 6 users not shown)

Line 1:

In [[theoretical computer science]] and [[mathematical logic]], specifically in [[realizability]], a '''partial combinatory algebra''' (pca) is an algebraic structure which can be viewed as an abstraction ofabstracts a [[model of computation]]. The definition of pcas uses an idea from [[combinatory logic]]. PcasThe are[[realizability usedtopos]] toover definea pca is a model of higher-order [[realizabilityintuitionistic toposlogic]]es where informally every function is computable in the model of computation specified by the pca.

==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> called ''application''. 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]]. {{r|van-oosten|p=1}}

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

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

* A variable, from some fixed, countably infinite set of variables <math>V</math>, is an expression,

* If <math>e_1</math> and <math>e_2</math> are expressions, then <math>e_1 e_2</math> is an expression.

(In other words, they form the [[free magma]] over the disjoint union <math>A + V</math> where <math>V</math> is the set of variables.)

A term is ''closed'' ifwhen 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> and <math>u</math> either do not evaluate to a defined value, or evaluate to the same value.

TheA partialsubstitution applicative structure ''A''operation is saidalso todefined bein ''combinatorythe complete''{{r|van-oosten|p=3}}natural or ''functionally complete''way: if, for every term <math>t(x_0, \dots, x_n)</math> (that is, a term, <math>tx</math> whoseis variablesa arevariable amongand <math>x_0,u</math> \dotsis another term, x_n<math>t[u/x]</math>), theredenotes existsthe an elementterm <math>at</math> \inwith all occurrences of A<math>x</math> suchreplaced that:by <math>u</math>.

The partial applicative structure ''A'' is said to be ''combinatory complete'' 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:{{r|bauer|p=27}}{{r|van-oosten|p=3}}

* <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 ⟶ 30:

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|bauer|p=28}}{{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 36 ⟶ 38:

For the proof, in the forward direction, if <math>A</math> is combinatory complete, it suffices to apply the definition of combinatory 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:{{r|van-oosten|p=3}}{{r|bauer|p=28}}

* <math>\langle x \rangle a = K a</math> for a constant <math>a \in A</math>,

Line 43 ⟶ 45:

* <math>\langle x \rangle (u v) = S (\langle x \rangle u) (\langle x \rangle v)</math>.

Beware that the analogy between <math>\langle x \rangle t</math> and <math>\lambda x \cdot t</math> is not perfect. For example, the terms <math>(\langle x \rangle t) t'</math> and <math>t[t'/x]</math> are not generally equivalent in a reasonable sense, e.g., taking a variable <math>y</math> different from <math>x</math> and <math>a, b \in A</math> constants, we have <math>(\langle x \rangle y)(a b) = K y (a b)</math>, which cannot be considered equivalent to <math>y</math> because the latter always evaluates to <math>c</math> if <math>y</math> is replaced by a constant <math>c \in A</math>, while the former may not as <math>a b</math> may be undefined.{{r|van-oosten|p=4–5}}

However, if <math>t'</math> is a constant <math>a</math>, then <math>(\langle x \rangle t) a</math> is indeed equivalent to <math>t[a/x]</math> in the sense that substituting all variables for some constants in these two terms gives the same result (per <math>\simeq</math>).{{r|van-oosten|p=4}}

Moreover, substituting variables by constants in <math>\langle x \rangle t</math> ''always'' evaluates to a defined result, even if this would not be the case by substituting variables in <math>t</math>. For example, if <math>a, b \in A</math> are two constants, the term <math>\langle x \rangle (a b)</math> (abstracting a variable which does not appear) is equal to <math>S (K a) (K b)</math>. By the assumptions on <math>K</math> and <math>S</math>, this is well-defined, even though <math>a b</math> may not be well-defined.{{r|van-oosten|p=4}}

These remarks imply that for all term <math>t(x_0, \dots, x_n)</math>, the value <math>a := \langle x_0 \rangle \dots \langle x_n \rangle t \downarrow</math> is well-defined and satisfies the two requirements of combinatory completeness.{{r|van-oosten|p=4}}

==Examples==

Line 55 ⟶ 57:

===First Kleene algebra===

The first Kleene algebra <math>\mathcal{K}_1</math> consists of the set <math>\mathbb{N}</math> with application <math>a b := \phi_a(b)</math>, where <math>\phi_a</math> denotes the <math>a</math>-th [[partial recursive function]] in a standard Gödel numbering.{{r|van-oosten|p=15}}{{r|bauer|p=29}}

This pca can also be [[relativization|relativized]] to an oracle <math>D \subseteq \mathbb{N}</math>: we define a pca <math>\mathcal{K}_1^D</math> with carrier <math>\mathbb{N}</math> by setting <math>a b := \phi^D_a(b)</math>, where <math>\phi^D_a</math> is the <math>a</math>-th partial recursive function with oracle <math>D</math>.{{r|van-oosten|p=15}}{{r|bauer|p=30}}

===Untyped λ-calculus===

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.{{r|van-oosten|p=23}}{{r|bauer|p=30}}

===Reflexive domains===

{{empty section|date=February 2025}}

===Second Kleene algebra===

{{empty section|date=February 2025}}

==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>

<ref name=bauer>{{ cite web | title = Notes on realizability | author = Andrej Bauer | website = [[GitHub]] | url = https://github.com/andrejbauer/notes-on-realizability/releases/download/release/notes-on-realizability.pdf | date = 2025-02-21 | access-date = 2025-02-21 }}</ref>

</references>

[[Category:Models of computation]]

{{mathlogic-stub}}