Content deleted Content added
m Copyedit |
m Avoid giving the idea that a topos is intensional for functions |
||
| (3 intermediate revisions by 2 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 abstracts a [[model of computation]]. The definition of pcas uses an idea from [[combinatory logic]]. The [[realizability topos]] over a pca is a model of higher-order [[intuitionistic logic]] where informally every function is
▲In [[theoretical computer science]] and [[mathematical logic]], specifically in [[realizability]], a '''partial combinatory algebra''' (pca) is an algebraic structure which abstracts a [[model of computation]]. The definition of pcas uses an idea from [[combinatory logic]]. The [[realizability topos]] over a pca is a model of higher-order [[intuitionistic logic]] where informally every function is a program in the pca's model of computation.
==Definition==
A ''partial applicative structure'' 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'' (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,
Line 18 ⟶ 17:
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>.
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>,
Line 31 ⟶ 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 39 ⟶ 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 46 ⟶ 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 58 ⟶ 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===
Line 76 ⟶ 75:
==References==
<references>
</references>
[[Category:Models of computation]]
| |||