 | This article needs additional citations for verification .(December 2012) |
The categorical abstract machine (CAM) is a model of computation for programs [1] that preserves the abilities of applicative, functional, or compositional style. It is based on the techniques of applicative computing.
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 for programmers, represented by Cartesian closed category 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 or lazy evaluation can be emulated as well as parameter passing, such as call by name, call by value, and so on. In theory, CAM preserves[ how? ] 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 the Categorical Abstract Machine Language. Both are variants of MetaLanguage ML, and all three languages implement type inference.
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. This comprehension arises as being influenced by the functional style of programming.
In mathematics and computer science, currying is the technique of converting a function that takes multiple arguments into a sequence of functions that each takes a single argument. For example, currying a function that takes three arguments creates three functions:
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program.
Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.
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 efficiently they can be solved or to what degree. The field is divided into three major branches: automata theory and formal languages, computability theory, and computational complexity theory, which are linked by the question: "What are the fundamental capabilities and limitations of computers?".
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.
A typed lambda calculus is a typed formalism that uses the lambda-symbol 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 type depends on the calculus considered. From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type.
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically valid strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically invalid strings, the result would be non-computation. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation.
Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science. The computability of a problem is closely linked to the existence of an algorithm to solve the problem.
Samson Abramsky is Professor of Computer Science at University College London. He has made contributions to the areas of domain theory, the lazy lambda calculus, strictness analysis, concurrency theory, interaction categories, geometry of interaction, game semantics and quantum computing.
In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.
The SKI combinator calculus is a combinatory logic system and a computational system. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. It can be likened to a reduced version of the untyped lambda calculus. It was introduced by Moses Schönfinkel and Haskell Curry.
Caml 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.
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages and of their individual features. It falls within the discipline of computer science, both depending on and affecting mathematics, software engineering, linguistics and even cognitive science. It has become a well-recognized branch of computer science, and an active research area, with results published in numerous journals dedicated to PLT, as well as in general computer science and engineering publications.
The following outline is provided as an overview of and topical guide to computer programming:
In computer science, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution. This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not expressed within the calculus; the "freshness" conditions in such implicit calculi are a notorious source of errors. The concept has appeared in a large number of published papers in quite different fields, such as in abstract machines, predicate logic, and symbolic computation.
Applicative computing systems, or ACS are the systems of object calculi founded on combinatory logic and lambda calculus. The only essential notion which is under consideration in these systems is the representation of object. In combinatory logic the only metaoperator is application in a sense of applying one object to other. In lambda calculus two metaoperators are used: application – the same as in combinatory logic, and functional abstraction which binds the only variable in one object.
The following outline is provided as an overview of and topical guide to formal science:
In theoretical computer science, the Krivine machine is an abstract machine. As an abstract machine, it shares features with Turing machines and the SECD machine. The Krivine machine explains how to compute a recursive function. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. Thanks to its formalism, it tells in details how a kind of reduction works and sets the theoretical foundation of the operational semantics of functional programming languages. On the other hand, Krivine machine implements call-by-name because it evaluates the body of a β-redex before it applies the body to its parameter. In other words, in an expression u it evaluates first λx. t before applying it to u. In functional programming, this would mean that in order to evaluate a function applied to a parameter, it evaluates first the function before applying it to the parameter.