Content deleted Content added
Added tags to the page using Page Curation (more footnotes) |
m Copyedit |
||
Line 4:
==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]].
The ''terms'' (or ''expressions'') over a partial applicative structure <math>A</math> are defined inductively:
| |||