CEK Machine

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

A CEK Machine is an abstract machine invented by Matthias Felleisen and Daniel P. Friedman. It is generally implemented as an interpreter for functional programming languages, but can also be used to implement simple imperative programming languages. A state in a CEK machine includes a control statement, environment and continuation. The control statement is the term being evaluated at that moment, the environment is (usually) a map from variable names to values, and the continuation stores another state, or a special halt case. It is a simplified form another abstract machine called the SECD machine.[1][2][3]

The CEK machine builds on the SECD machine by replacing the dump (call stack) with the more advanced continuation, and putting parameters directly into the environment, rather than pushing them on to the parameter stack first. Other modifications can be made which creates a whole family of related machines. For example, the CESK machine has the environment map variables to a pointer on the store, which is effectively a heap. This allows it to model mutable state better than the ordinary CEK machine. The CK machine has no environment, and can be used for simple calculi without variables.[4]

Description[edit]

A CEK machine can be created for any programming language so the term is often used vaguely. For example, a CEK machine could be created to interpret the lambda calculus. Its environment maps variables to closures and the continuations are either a halt, a continuation to evaluate an argument (ar), or a continuation to evaluate an application after evaluating a function (ap):[3][5]

Transition From To
Variable x, E, K t, E', K where closure(t,E') = E[x]
Application (f e), E, K f, E, ar(e, E, K)
Abstraction while evaluating function Abs, E, ar(t, E', K) t, E', ap(Abs, E, K)
Abstraction while evaluating argument Abs, E, ap(λx.Exp, E', K) Exp, E[x=closure(Abs,E)], K

Representation of components[edit]

Each component of the CEK machine has various representations. The control string is usually a term being evaluated, or sometimes, a line number. For example, a CEK machine evaluating the lambda calculus would use a lambda expression as a control string. The environment is almost always a map from variables to values, or in the case of CESK machines, variables to addresses in the store. The representation of the continuation varies. It often contains another environment as well as a continuation type, for example argument or application. It is sometimes a call stack, where each frame is the rest of the state, i.e. a control statement and an environment.

Related machines[edit]

There are some other machines closely linked to the CEK machine.

CESK machine[edit]

The CESK machine is another machine closely related to the CEK machine. The environment in a CESK machine maps variables to pointers, on a "store" (heap) hence the name "CESK". It can be used to model mutable state, for example the Λσ calculus described in the original paper. This makes it much more useful for interpreting imperative programming languages, rather than functional ones.[4]

CS machine[edit]

The CS machine contains just a control statement and a store. It is also described by the original paper. In an application, instead of putting variables into an environment it substitutes them with an address on the store and putting the value of the variable in that address. The continuation is not needed because it is lazily evaluated; it does not need to remember to evaluate an argument.[4]

SECD machine[edit]

The SECD machine was the machine that CEK machine was based on. It has a stack, environment, control statement and dump. The dump is a call stack, and is used instead of a continuation. The stack is used for passing parameters to functions. The control statement was written in postfix notation, and the machine had its own "programming language". A lambda calculus statement like this:

(M N)

would be written like this:

N:M:ap

where ap is a function that applies two abstractions together.[6][7]

References[edit]

  1. ^ Jens Palsberg (28 August 2009). Semantics and Algebraic Specification: Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday. Springer Science & Business Media. pp. 162–. ISBN 978-3-642-04163-1.
  2. ^ Matthias Felleisen; Robert Bruce Findler; Matthew Flatt (10 July 2009). Semantics Engineering with PLT Redex. MIT Press. pp. 113–. ISBN 978-0-262-25817-3.
  3. ^ a b Thielecke, Hayo (December 9, 2015). "Implementing functional languages with abstract machines" (PDF). Retrieved September 9, 2020.
  4. ^ a b c Felleisen, Matthias; Friedman, Daniel (October 1986). "A Calculus for Assignments in Higher-Order Languages" (PDF).
  5. ^ "A refresher on the CEK machine". CMSC 330, Summer 2015. Retrieved 2020-09-19.
  6. ^ "The SECD Virtual Machine" (PDF).
  7. ^ "secd". www.cs.bath.ac.uk. Retrieved 2020-09-23.