Applicative structures

An applicative structure is a minimal setting which models the concept of function application.

Applicative structures are widely used in the semantics of \lambda-calculi, and various type theories.

Untyped applicative structures

An (untyped) applicative structure consists of

1. a set D
2. an binary operation, \cdot : D \times D \to D

As witnessed, this is the simplest set-theoretic structure that can model a domain of elements d \in D, each of which can be seen as a function d \cdot - : D \to D on that very domain itself.

We can also distinguish extensional applicative structures. An applicative structure is extensional whenever for all x \in D we have that d_1 \cdot x = d_2 \cdot x, then we can conclude that d_1 = d_2. That is, if d_1 \cdot - and d_2 \cdot - are the same function, then the elements d_1, d_2 \in D must be identical.

Typed applicative structures

A definition of applicative structures can also be given in a typed setting.

For simplicity, we only consider the finite type structure over a base type \iota. These are generated by the grammar

\sigma, \tau\ ::=\ \iota\ |\ \sigma \to \tau

A typed applicative structure consists of

1. A family of sets \{D_\sigma\}_\sigma indexed in finite types.
2. For each pair of types \sigma, \tau a function

\textsf{App}_{\sigma, \tau} : D_{\sigma \to \tau} \times D_\sigma \to D_\tau

A typed applicative structure is extensional if the following condition holds: given any f, g \in D_{\sigma \to \tau}, if we have \textsf{App}_{\sigma, \tau}(f, x) = \textsf{App}_{\sigma, \tau}(g, x) for all x \in D_\sigma, then we can conclude that f = g.

See also

• Combinatory algebras
• Partial applicative structures

References

• Untyped applicative structures are defined in §5.1 of

@book{barendregt_1984,
	address = {Amsterdam},
	title = {Lambda {Calculus}: {Its} {Syntax} and {Semantics}},
	isbn = {978-0-444-87508-2},
	publisher = {North-Holland},
	author = {Barendregt, Henk},
	year = {1984}
}

Is it known if they predate Barendregt?

• Typed applicative structures are introduced under the name pre-structures in Harvey Friedman's classic paper on completeness of set-theoretic models of simple types.

@inproceedings{friedman_1975,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Mathematics}},
	title = {Equality between functionals},
	volume = {453},
	doi = {10.1007/BFb0064870},
	booktitle = {Logic {Colloquium}},
	publisher = {Springer Berlin Heidelberg},
	author = {Friedman, Harvey},
	editor = {Dold, A. and Eckmann, B. and Parikh, Rohit},
	year = {1975},
	pages = {22--37}
}