An applicative structure is a minimal setting which models the concept of function application.
Applicative structures are widely used in the semantics of -calculi, and various type theories.
An (untyped) applicative structure consists of
As witnessed, this is the simplest set-theoretic structure that can model a domain of elements , each of which can be seen as a function on that very domain itself.
We can also distinguish extensional applicative structures. An applicative structure is extensional whenever for all we have that , then we can conclude that . That is, if and are the same function, then the elements must be identical.
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 . These are generated by the grammar
A typed applicative structure consists of
A typed applicative structure is extensional if the following condition holds: given any , if we have for all , then we can conclude that .
Barendregt, Henk. 1984. Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland. [link]
@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?
Friedman, Harvey. 1975. ‘Equality between Functionals’. In Logic Colloquium, edited by Rohit Parikh, 453:22–37. Lecture Notes in Mathematics. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0064870.
@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}
}