categorical abstract machine
   HOME

TheInfoList



OR:

The categorical abstract machine (CAM) is a
model of computation In computer science, and more specifically in computability theory and computational complexity theory, a model of computation is a model which describes how an output of a mathematical function is computed given an input. A model describes how ...
for programs''Cousineau G., Curien P.-L., Mauny M.'' The categorical abstract machine. — LNCS, 201, Functional programming languages computer architecture.-- 1985, pp.~50-64. that preserves the abilities of applicative, functional, or compositional style. It is based on the techniques of applicative computing.


Overview

The notion of the categorical abstract machine arose in the mid-1980s. It took its place in computer science as a kind of
theory of computation In theoretical computer science and mathematics, the theory of computation is the branch that deals with what problems can be solved on a model of computation, using an algorithm, how algorithmic efficiency, efficiently they can be solved or t ...
for programmers, represented by
Cartesian closed category In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in math ...
and embedded into the combinatory logic. CAM is a transparent and sound mathematical representation for the languages of functional programming. The machine code can be optimized using the equational form of a theory of computation. Using CAM, the various mechanisms of computation such as
recursion Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathemati ...
or
lazy evaluation In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed ( non-strict evaluation) and which also avoids repeated evaluations (sharing). The ...
can be emulated as well as parameter passing, such as
call by name In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the f ...
,
call by value In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the f ...
, and so on. In theory, CAM preserves all the advantages of object approach towards programming or computing. The main current implementation is OCaml, which added class inheritance and dynamic method dispatch to
Caml Caml (originally an acronym for Categorical Abstract Machine Language) is a multi-paradigm, general-purpose programming language which is a dialect of the ML programming language family. Caml was developed in France at INRIA and ENS. Caml is ...
the Categorical Abstract Machine Language. Both are variants of MetaLanguage ML, and all three languages implement
type inference Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistic ...
.


Implementation

One of the implementation approaches to functional languages is given by the machinery based on supercombinators, or an SK-machine, by D. Turner. The notion of CAM gives an alternative approach. The structure of CAM consists of syntactic, semantic, and computational constituents. Syntax is based on de Bruijn’s notation, which overcomes the difficulties of using bound variables. The evaluations are similar to those of P. Landin’s SECD machine. With this coverage, CAM gives a sound ground for syntax, semantics, and
theory of computation In theoretical computer science and mathematics, the theory of computation is the branch that deals with what problems can be solved on a model of computation, using an algorithm, how algorithmic efficiency, efficiently they can be solved or t ...
. This comprehension arises as being influenced by the functional style of programming.


See also

* Combinatory logic *
Typed lambda calculus A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a ...
*
Cartesian closed category In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in math ...
* Applicative computing systems *
Anonymous recursion In computer science, anonymous recursion is recursion which does not explicitly call a function by name. This can be done either explicitly, by using a higher-order function – passing in a function as an argument and calling it – or implicitly ...
*
Evaluation strategy In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the f ...
*
Explicit substitution In computer science, lambda calculus, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution of variables, substitution. This is in contrast to the standard lambda cal ...
* SKI combinator calculus *
Unlambda Unlambda is a minimal, "nearly Purely functional language, pure" functional programming language invented by David Madore. It is based on combinatory logic, an expression system without the Lambda calculus, lambda operator or free variables. It r ...
* Currying *
Caml Caml (originally an acronym for Categorical Abstract Machine Language) is a multi-paradigm, general-purpose programming language which is a dialect of the ML programming language family. Caml was developed in France at INRIA and ENS. Caml is ...


References


Further reading

* Wolfengagen, V.E.
Combinatory Logic in Programming
Computations with Objects through Examples and Exercises''. 2nd ed. M.: "Center JurInfoR" Ltd., 2003. x+337 с. {{ISBN, 5-89158-101-9. Implementation of functional programming languages Models of computation Applicative computing systems