Applicative transition system

An applicative transition system (ATS) is a structure that models an untyped \lambda-calculus as a state transition system.

Definition (lazy)

The original definition of an ATS comes from Abramsky 1990, and concerns lazy untyped \lambda-calculus.

A quasi-applicative transition system (qATS) (\textsf{ev}, A) consists of a set A and a partial function

  \textsf{ev} : A \rightharpoonup (A \to A)

We write a \Downarrow f whenever \textsf{ev}(a) \simeq f, where \simeq is Kleene equality.

The function \textsf{ev} interprets some elements of A as functions over A. These can be seen as state transition functions.

Based on a qATS, we may define a relation x \lesssim y on A that means that y simulates x under applicative simulation.

An ATS is then defined as a qATS that preserves applicative simulation, in the sense that a \Downarrow f and x \lesssim y implies f(x) \lesssim f(y).

Definition (call-by-value, effectful)

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 (\textsf{Set}-)monad T is defined to consist of

• a set \mathcal{V} of values
• a set \mathcal{X} of computations
• an evaluation function \textsf{eval} : \mathcal{X} \to T(\mathcal{V}) mapping computations to monadic values
• and an application function \mathbin{\cdot} : \mathcal{V} \times \mathcal{V} \to \mathcal{X} for applying two values.

References

@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}
}

@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}
}