Reduction strategy (lambda calculus)

Last updated

In lambda calculus, a branch of mathematical logic concerned with the formal study of functions, a reduction strategy is how a complex expression is reduced to a simple expression by successive reduction steps. It is similar to but subtly different from the notion of evaluation strategy in computer science.

Contents

Overview

Roughly, a reduction strategy is a function that maps a lambda calculus term with reducible expressions to one particular reducible expression, the one to be reduced next. Mathematical logicians have studied the properties of this system for decades, and the superficial similarity between the description of evaluation strategies and reduction strategies originally misled programming language researchers to speculate that the two were identical, a belief that is still visible in popular textbooks from the early 1980s; [1] these are, however, different concepts.[ citation needed ]

Plotkin [2] showed in 1973, however, that a proper model of an evaluation strategy calls for the formulation of a new axiom for function calls, that is, an entirely new calculus. He validates this idea with two different calculi: one for call-by-name and another one for call-by-value, each for purely functional programming languages. He also shows that such a calculus satisfies two natural criteria. First, a calculus defines an evaluation function that maps closed terms (representations of programs) to answers (representations of outputs). This theorem relies on a conventional Church–Rosser theorem for the modified calculus. The evaluation function is defined via the traditional Curry–Feys standardization theorem. Second, the calculus is a sound equational reasoning system with respect to Morris' notion of observational equivalence. [3]

Twenty years later, Crank and Felleisen showed how to scale Plotkin's work to languages with imperative assignment statements. [4] They define calculi for a language with variables, functions, function application and assignment statement that capture the conventional notions of parameter passing and evaluation strategies of a wide array of programming languages. They show that each calculus satisfies Plotkin's criteria, including traditional Church–Rosser and Curry–Feys theorems respectively. In addition, they introduce a calculus that reifies ML's notion of reference cell.

Ariola and Felleisen [5] and independently Maraist, Odersky and Wadler [6] completed this line of work with the design of a lambda calculus that precisely relates the notion of call-by-need aka lazy functional programming to an equational system of calculation. Unlike Plotkin's call-by-value and call-by-name calculi, this call-by-need calculus requires four axioms to characterize function calls. Chang and Felleisen [7] were eventually able to show how to create a by-need calculus with a single, but complex axiom.

See also

Related Research Articles

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 each return a value, rather than a sequence of imperative statements which change the state of the program.

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 and which also avoids repeated evaluations (sharing). The sharing can reduce the running time of certain functions by an exponential factor over other non-strict evaluation strategies, such as call-by-name, which repeatedly evaluate the same function, blindly, regardless whether the function can be memoized.

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.

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.

Church–Rosser theorem theorem

In mathematics and theoretical computer science, the Church–Rosser theorem states that, when applying reduction rules to terms in some variants of the lambda calculus, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying sequences of additional reductions. The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser, after whom it is named.

In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function. In combinatory logic for computer science, a fixed-point combinator is a higher-order function that returns some fixed point of its argument function, if one exists.

Curry's paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself "If C, then F", requiring only a few apparently innocuous logical deduction rules. Since F is arbitrary, any logic having these rules allows one to prove everything. The paradox may be expressed in natural language and in various logics, including certain forms of set theory, lambda calculus, and combinatory logic.

Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.

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 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 simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.

Evaluation strategies are used by programming languages to determine two things—when to evaluate the arguments of a function call and what kind of value to pass to the function.

Programming language theory Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of 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.

In mathematical logic and computer science, the lambda-mu calculus is an extension of the lambda calculus introduced by M. Parigot. It introduces two new operators: the μ operator and the bracket operator. Proof-theoretically, it provides a well-behaved formulation of classical natural deduction.

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 concept of explicit substitutions has become notorious because the notion often turns up in formal descriptions and implementation of all the mathematical forms of substitution involving variables such as in abstract machines, predicate logic, and symbolic computation.

Formal definitions of the lambda calculus. Lambda calculus is a programming language based on lambda abstraction and function application. Two definitions of the language are given here.

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.

References

  1. ↑ Structure and Interpretation of Computer Programs by Abelson and Sussman, MIT Press 1983
  2. ↑ Call-by-name, call-by-value, and the lambda calculus
  3. ↑ "Programming languages and lambda calculus by James Morris, MIT 1968"
  4. ↑ Parameter-Passing and the Lambda Calculus by Crank and Felleisen, Principles of Programming Languages 1991
  5. ↑ The call-by-need lambda calculus by Ariola and Felleisen, Journal of Functional Programming 1997
  6. ↑ The call-by-need lambda calculus by Maraist Odersky and Wadler, Journal of Functional Programming 1999
  7. ↑ The call-by-need lambda calculus, revisited by Chang and Felleisen, European Symposium on Programming, 2012
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.