An applicative transition system (ATS) is a structure that models an untyped -calculus as a state transition system.
The original definition of an ATS comes from [Abramsky 1990], and concerns lazy untyped -calculus.
A quasi-applicative transition system (qATS) consists of a set and a partial function
We write whenever , where is Kleene equality.
The function interprets some elements of as functions over . These can be seen as state transition functions.
Based on a qATS, we may define a relation on that means that simulates under applicative simulation.
An ATS is then defined as a qATS that preserves applicative simulation, in the sense that and implies .
[Dal Lago et al. 2017] have presented a monadic CBV variant of a qATS, which is appropriate for effectful CBV languages. The definition of a qATS is adapted to support both values and computations.
A monadic, CBV qATS over a (-)monad is defined to consist of
Abramsky, Samson. “The Lazy Lambda Calculus.” In Research Topics in Functional Programming, 65–117. Addison Wesley, 1990. [pdf]
@incollection{abramsky_1990,
title = {The Lazy Lambda Calculus},
url = {https://www.cs.ox.ac.uk/files/293/lazy.pdf},
pages = {65--117},
booktitle = {Research Topics in Functional Programming},
publisher = {Addison Wesley},
author = {Abramsky, Samson},
date = {1990}
}
Dal Lago, Ugo, Francesco Gavazzo, and Paul Blain Levy. “Effectful Applicative Bisimilarity: Monads, Relators, and Howe’s Method.” In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2017. https://doi.org/10.1109/LICS.2017.8005117.
@inproceedings{dal_lago_effectful_2017,
title = {Effectful applicative bisimilarity: Monads, relators, and Howe's method},
doi = {10.1109/LICS.2017.8005117},
booktitle = {2017 32nd Annual {ACM}/{IEEE} Symposium on Logic in Computer Science ({LICS})},
publisher = {{IEEE}},
author = {Dal Lago, Ugo and Gavazzo, Francesco and Levy, Paul Blain},
date = {2017},
archivePrefix = {arXiv},
eprint = {1704.04647}
}