Lambda Calculus

10 Key excerpts on "Lambda Calculus"

• 

  No longer available |Learn more

  Introduction to Theory of Computation, An

  • (Author)
  • 2014(Publication Date)
  • Learning Press

    (Publisher)

  A particular challenge is related to the support of higher-order functions, also known as the Funarg problem. Lambda Calculus is usually implemented using a virtual machine approach. The first practical implementation of Lambda Calculus was provided in 1963 by Peter Landin, and is known as the SECD machine. Since then, several optimized abstract machines for Lambda Calculus were suggested, such as the G-machine and the categorical abstract mac-hine. The most prominent counterparts to Lambda Calculus in programming are functional pro-gramming languages, which essentially implement the calculus augmented with some constants and datatypes. Lisp uses a variant of lambda notation for defining functions, but only its purely functional subset (Pure Lisp) is really equivalent to Lambda Calculus. First-class functions Anonymous functions are sometimes called lambda expressions in programming lan-guages. An example of the 'square' function as a lambda expression in Lisp: ( lambda (x) (* x x)) or Haskell: ________________________ WORLD TECHNOLOGIES ________________________ x -> x*x -- where the denotes the greek λ The above Lisp example is an expression which evaluates to a first-class function. The symbol lambda creates an anonymous function, given a list of parameter names, (x) — just a single argument in this case, and an expression which is evaluated as the body of the function, (* x x) . The Haskell example is identical. Functional languages are not the only ones to support functions as first-class objects. Numerous imperative languages, e.g. Pascal, have long supported passing subprograms as arguments to other subprograms. In C and the C-like subset of C++ the equivalent result is obtained by passing pointers to the code of functions (subprograms) deemed function pointers. Such mechanisms are limited to subprograms written explicitly in the code, and do not directly support higher-level functions.

  Sign up to read

  Learn more about book
• 

  eBook - PDF

  Artificial and Mathematical Theory of Computation

  Papers in Honor of John McCarthy

  • Vladimir Lifschitz(Author)
  • 2012(Publication Date)
  • Academic Press

    (Publisher)

  It imposes structure on denotational defini-tions that can be exploited in language implementations, most notably the generation of compilers from denotational definitions [9, 10, 15, 16]. The critical idea underlying our interpretation of the Lambda Calculus is that λ should be interpreted as a function instead of a syntactic marker. This modification has three major consequences: • the universe of the model must be enlarged to include environments, • variables must be interpreted as selector functions mapping environ-ments to values, and • every primitive operation / on program data must be reinterpreted as the abstracted function / ' defined by the equation (f f p = / ) , where ρ is an arbitrary environment. Fortunately, the resulting system is easily understood and intuitively natu-ral. In fact, this interpretation of the λ-calculus can be viewed as a higher-order generalization of Backus's functional programming language FP [2], where • functions map records (representing environments) rather than se-quences to values, and • functions (denoted by λ-expressions) can be passed as arguments to other functions and returned as the values of function applications. 2 Technical Preliminaries The terminology in this chapter is consistent with the conventions estab-lished by Barendregt [3], except for the definition of λ-calculus models given in Section 3. Our formulation of λ-calculus models differs from Baren-dregt because the λ-calculus does not qualify as an idealized functional Lambda: the Ultimate Combinator 29 programming language unless it includes primitive operations for manipu-lating ground data values (e.g. integers) that are not functions. This chapter presumes some familiarity with the rudiments of domain theory [11, 12], universal algebra [5], and the λ-calculus [3]. In subsequent discussions involving domains, the term domain refers to an arbitrary cpo (complete partial order). The least element of a cpo is denoted by the symbol J_.

  Sign up to read

  Learn more about book
• 

  eBook - ePub

  Alan Turing

  His Work and Impact

  • S. Barry Cooper, J. van Leeuwen(Authors)
  • 2013(Publication Date)
  • Elsevier Science

    (Publisher)

  λ -Definability*

  Henk Barendregt, Giulio Manzonetto and Rinus Plasmeijer trace through to today — The Imperative and Functional Programming Paradigm

  (J. Symbolic Logic, vol. 2 (1937), p. 153–163)

  1 Models of computation

  In Turing (1936) a characterisation is given of those functions that can be computed using a mechanical device. Moreover it was shown that some precisely stated problems cannot be decided by such functions. In order to give evidence for the power of this model of computation, Turing (1937) showed that machine computability has the same strength as definability via λ -calculus, introduced in Church (1936) . This model of computation was also introduced with the aim of showing that undecidable problems exist.

  Turing machine computability forms a very simple model that is easy to mechanise. Lambda Calculus computability, on the other hand, is a priori more powerful. Therefore, it is not obvious that it can be executed by a machine. In showing the equivalence of both models, Turing shows us that λ -calculus computations are performable by a machine, so demonstrating the power of Turing machine computations. This gave rise to the combined

  Church-Turing Thesis The notion of intuitive computability is exactly captured by λ -definability or by Turing computability .

  Computability via Turing machines gave rise to imperative programming. Computability described via λ -calculus gave rise to functional programming. As imperative programmes are more easy to run on hardware, this style of software became predominant. We present major advantages of the functional programming paradigm over the imperative one, that are applicable, provided one is willing to explicitly deal with simple abstractions.

  2 Functional programming

  2.1 Features from Lambda Calculus

  Rewriting . Lambda terms form a set of formal expressions subjected to possible rewriting (or reduction

  Sign up to read

  Learn more about book
• 

  eBook - PDF

  Lambda-Calculus and Combinators

  An Introduction

  • J. Roger Hindley, Jonathan P. Seldin(Authors)
  • 2008(Publication Date)
  • Cambridge University Press

    (Publisher)

  1 The λ-calculus 1A Introduction What is usually called λ-calculus is a collection of several formal systems, based on a notation invented by Alonzo Church in the 1930s. They are designed to describe the most basic ways that operators or functions can be combined to form other operators. In practice, each λ-system has a slightly different grammatical struc- ture, depending on its intended use. Some have extra constant-symbols, and most have built-in syntactic restrictions, for example type-restrict- ions. But to begin with, it is best to avoid these complications; hence the system presented in this chapter will be the ‘pure’ one, which is syntactically the simplest. To motivate the λ-notation, consider the everyday mathematical ex- pression ‘x − y’. This can be thought of as defining either a function f of x or a function g of y; f (x) = x − y, g(y) = x − y, or f : x → x − y, g : y → x − y. And there is a need for a notation that gives f and g different names in some systematic way. In practice, mathematicians usually avoid this need by various ‘ad-hoc’ special notations, but these can get very clumsy when higher-order functions are involved (functions which act on other functions). Church’s notation is a systematic way of constructing, for each expres- sion involving ‘x’, a notation for the corresponding function of x (and similarly for ‘y’, etc.). Church introduced ‘λ’ as an auxiliary symbol and 1 2 The λ-calculus wrote f = λx . x − y g = λy . x − y. For example, consider the equations f (0) = 0 − y, f (1) = 1 − y. In the λ-notation these become (λx . x − y)(0) = 0 − y, (λx . x − y)(1) = 1 − y. These equations are clumsier than the originals, but do not be put off by this; the λ-notation is principally intended for denoting higher-order functions, not just functions of numbers, and for this it turns out to be no worse than others. 1 The main point is that this notation is system- atic, and therefore more suitable for incorporation into a programming language.

  Sign up to read

  Learn more about book
• 

  eBook - PDF

  Language and Logics

  An Introduction to the Logical Foundations of Language

  • Howard Gregory(Author)
  • 2015(Publication Date)
  • Edinburgh University Press

    (Publisher)

  67 chapter 5 FUNCTIONS: THE Lambda Calculus This chapter introduces one of the main contributions of Richard Montague to lin-guistics, known as Montague semantics. (It also had an influence on syntax, on which context it is usually called Montague Grammar.) Montague’s own presentation of his work (three short papers, published after his early death in 1971) is notoriously and unnecessarily difficult. However, it has been reworked by a number of excellent writers since then into a more digestible form, and it is this tradition that is drawn on here. The end of the last chapter introduced the distinction between first order and higher order logics. One of the cornerstones of Richard Montague’s programme for semantics was the use of higher order logic. Montague semantics in general (and its developments, such as Generalized Quantifier Theory) are not covered by this book. However, this chapter will introduce his influential choice for a logical translation language: the simply typed Lambda Calculus , which is the basis for many of the ideas discussed in the rest of the book. 1 The Lambda Calculus is a theory of functions. Functions have been discussed already in earlier chapters; however, from now on they will take centre stage, and it is important to consolidate some basic notions. A function is a process that acts on an input (the argument ) to produce an output (the value ). Feeding an argument to a function to get a value is called function application – the function is applied to the argument. If a function f is applied to an argument a to give a value v , then the normal notation for this is f(a) = v . (5.1) 1. capital-of(scotland) = edinburgh 2. square-of(4) = 16 3. mother-of(william) = diana As we also saw in Chapter 3, a function can also be seen – and written – as a binary relation, subject to particular constraints. In this case the same function can be written F(v, a) (5.2).

  Sign up to read

  Learn more about book
• 

  eBook - PDF

  Lambda Calculus with Types

  • Henk Barendregt, Wil Dekkers, Richard Statman(Authors)
  • 2013(Publication Date)
  • Cambridge University Press

    (Publisher)

  Many se- rious applications are written in these languages. The interactive aspect of both languages is made possible by lazy evaluation and the use of higher- type 7 functions, two themes that are at the core of the Lambda Calculus (λK, that is). It is to be expected that they will have a significant impact on the production of modern (interactive window-based) software. Other aspects of functional programming In several of the following viable applications there is a price to pay. Types can no longer be derived by the Hindley–Milner algorithm, but need to be deduced by an assignment system more complex than that of the simply typed λ-calculus λ → . Type classes Certain types come with standard functions or relations. For example on the natural numbers and integers one has the successor function, and the 7 In the functional programming community these are called ‘higher-order functions’. We prefer to use the more logically correct expression ‘higher-type’ , since ‘higher-order’ refers to quan- tification over types (like in the system λ2). 340 Applications equality and order relations. A type class is like a signature in computer science or a similarity type in logic: it states to which operations, constants, and relations the data type is coupled. In this way one can write programms not for one type but for a class of types. If the operators on classes are not only first order but higher order, one obtains ‘type constructor classes’, that are much more powerful. See Jones (1993), where the idea was introduced and Voigtl¨ ander (2009) for recent results. Generic programming The idea of type classes can be pushed further. Even if data types are differ- ent, in the sense that they have different constructors, one can share code. For [a 0 , a 1 , a 2 , . . . ] a stream, there is the higher type function ‘map s ’ that acts like map s f[a 0 , a 1 , a 2 , . . . ]  [fa 0 , fa 1 , fa 2 , . . . ].

  Sign up to read

  Learn more about book
• 

  eBook - ePub

  Logic from Russell to Church

  • Dov M. Gabbay, John Woods(Authors)
  • 2009(Publication Date)
  • North Holland

    (Publisher)

  Lambda-Calculus and Combinators in the 20th Century

  Felice Cardone; J. Roger Hindley

  1 INTRODUCTION

  The formal systems that are nowadays called λ -calculus and combinatory logic were both invented in the 1920s, and their aim was to describe the most basic properties of function-abstraction, application and substitution in a very general setting. In λ -calculus the concept of abstraction was taken as primitive, but in combinatory logic it was defined in terms of certain primitive operators called basic combinators.

  The present article will sketch the history of these two topics, until approximately the year 2000.

  We shall assume the reader is familiar with at least one of the many versions of these systems in the current literature. A few key technical details will be given as footnotes, however.1 Often “combinatory logic” will be abbreviated to “CL” and “λ -calculus” to “λ ”. We shall distinguish between “pure” versions of λ or CL (theories of conversion or reduction with nothing more) and “applied” versions (containing extra concepts such as logical constants, types or numbers).

  To understand the early history it is worth remembering that the situation in logic and the foundations of mathematics was much more fluid in the early 1900s than it is today; Russell’s paradox was relatively recent, Gödel’s theorems were not yet known, and a significant strand of work in logic was the building of systems intended to be consistent foundations for the whole of mathematical analysis. Some of these were based on a concept of set, others on one of function, and there was no general consensus as to which basis was better. In this context λ and CL were originally developed, not as autonomous systems but as parts of more elaborate foundational systems based on a concept of function.

  Today, λ and CL are used extensively in higher-order logic and computing. Rather like the chassis of a bus, which supports the vehicle but is unseen by its users, versions of λ or CL underpin several important logical systems and programming languages. Further, λ

  Sign up to read

  Learn more about book
• 

  eBook - ePub

  Get Programming with Haskell

  • Will Kurt(Author)
  • 2018(Publication Date)
  • Manning

    (Publisher)

  Lambda Calculus. In Lambda Calculus, you represent everything as functions: true and false are functions, and even all the integers can be represented as functions.

  Church’s goal was initially to resolve some problems in the mathematical field of set theory. Unfortunately, Lambda Calculus didn’t solve these problems, but something much more interesting came out of Church’s work. It turns out that Lambda Calculus allows for a universal model of computation, equivalent to a Turing machine!

  What is a Turing machine?

  A Turing machine is an abstract model of a computer developed by the famous computer scientist Alan Turing. From a theoretical standpoint, the Turing machine is useful because it allows you to reason about what can and can’t be computed, not just on a digital computer, but any possible computer. This model also allows computer scientists to show equivalence between computing systems if they can each simulate a Turing machine. You can use this to show, for example, that there’s nothing that you can compute in Java that you can’t also compute in assembly language.

  This discovery of the relationship between Lambda Calculus and computing is called the Church-Turing thesis (for more information, see www.alanturing.net/turing_archive/pages/reference%20articles/The%20Turing-Church%20Thesis.html ). The wonderful thing about this discovery is that you have a mathematically sound model for programming!

  Most programming languages that you use are marvelous pieces of engineering but provide little assurance about how programs will behave. With a mathematical foundation, Haskell is able to remove entire classes of bugs and errors from the code you write. Cutting-edge research in programming languages is experimenting with ways to mathematically prove that programs will do exactly what you expect. Additionally, the nonmathematical nature of most programming language designs means the abstractions you can use are limited by engineering decisions in the language. If you could program math, you’d be able to both prove things about your code and have access to the nearly limitless abstractions that mathematics allows. This is the aim of functional programming: to bring the power of mathematics to the programmer in a usable way.

  Sign up to read

  Learn more about book
• 

  No longer available |Learn more

  A++ and the Lambda Calculus

  Principles of Functional Programming

  • Georg P. Loczewski(Author)
  • 2018(Publication Date)
  • tredition

    (Publisher)

  XVI . The following phrase puts everything to a point:

  Abstraction is all there is to talk about: it is both the object and the means of discussion. Guy L. Steele Jr .

  ARS provides a base for imperative programming and object-oriented programming as well and can be applied to programming in almost any programming language.

  ARS , the basic operations of the Lambda Calculus in their generalized form are defined as follows:

  Abstraction: Give something a name.

  Reference: Reference an abstraction by name.

  Synthesis: Combine two or more abstractions to create something new.

  These operations may sound rather trivial and abstract but taken as principles of programming they change the style and method of programming thoroughly.

  The generalization of the Lambda Calculus consists in defining the concept of abstraction simply by ‘give something a name’. The name hides all the details of the defined. Abstraction thus defined requires an explicit definition of a name .

  The Lambda Calculus does not allow for an explicit definition of a name. The only possibility to associate a name to a value in the Lambda Calculus is by calling a function with an argument. This operation corresponds to the synthesis operation however and not to the creation of an abstraction. Lambda-abstractions in the Lambda Calculus are ‘per se’ anonymous.

  Sign up to read

  Learn more about book
• 

  eBook - PDF

  Provability, Computability and Reflection

  • Lev D. Beklemishev(Author)
  • 2000(Publication Date)
  • Elsevier Science

    (Publisher)

  CHAPTER 3 Lambda-Conversion We have seen in 3 OC that the theory of lambda-conversion occupies a position intermediate between ordinary logic and the theory of combi- nators, and that it is convenient to begin the study of combihatory logic with the former. Accordingly we shall devote the present chapter to it. There are several forms of lambda-conversion which we shall treat con- currently; hence we shall speak somewhat indifferently of a calculus or of calculuses of lambda-conversion. We shall begin (5 A) with an intuitive discussion of variables in mathe- matics (which will amplify somewhat the discussion in 3 OA and 9 2C). Then we shall introduce the idea of functional abstraction ( 3 B) and the rules for it; after that the operation of application. Proceeding in the direction from the intuitive to the formal, we arrive at the calculus formulated as a formal system in $$ C-D. A full formulation of the calculus as formal system will include, in 9 E, a rigorous theory of the prefixes of substitution, such that substitution is always defined; since any sort of bound variables can be defined in terms of functional abstrac- tion, this will simplify the statement of substitution rules in several theories. Examples of the technique of A-conversion will be found in Chapter 5. We leave for Chapter 4 the formulation and proof of the consistency theorem of Church and Rosser. A. VARIABLES AND FUNCTIONS I N MATHEMATICS In this section we discuss intuitively the role of formal variables in mathematics. The discussion may be compared with the introductory portions of various papers by Church, with the treatment of the same topic in Rosser [LMth], and with the writings of Menger. 1. Elementary examples From the discussions of Chapter 2 and the Introduction it is evident that formal variables are employed in logical systems to indicate substi- tution processes. Combinatory logic is thus concerned with the analysis of formal variables and their eventual elimination.

  Sign up to read

  Learn more about book