Misplaced Pages

#954045

58-462: The machine was the first to be specifically designed to evaluate lambda calculus expressions. It was originally described by Peter J. Landin in "The Mechanical Evaluation of Expressions" in 1964. The description published by Landin was fairly abstract, and left many implementation choices open (like an operational semantics ). Lispkit Lisp was an influential compiler based on the SECD machine, and

116-766: A capture-avoiding manner. This is defined so that: For example, ( λ x . x ) [ y := y ] = λ x . ( x [ y := y ] ) = λ x . x {\displaystyle (\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x} , and ( ( λ x . y ) x ) [ x := y ] = ( ( λ x . y ) [ x := y ] ) ( x [ x := y ] ) = ( λ x . y ) y {\displaystyle ((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y} . The freshness condition (requiring that y {\displaystyle y}

174-402: A cell holding 2 and at cell 7, which represents the list containing only 3 . It does so by pointing at cell 8 containing the value 3 , and pointing at an empty list ( nil ) as cdr. In the SECD machine, cell 0 always implicitly represents the empty list, so no special tag value is needed to signal an empty list (everything needing that can simply point to cell 0). The principle that the cdr in

232-414: A list cell must point at another list is just a convention. If both car and cdr point at atoms, that will yield a pair, usually written like (1 . 2) A number of additional instructions for basic functions like car, cdr, list construction, integer addition, I/O, etc. exist. They all take any necessary parameters from the stack. Lambda calculus Lambda calculus (also written as λ -calculus )

290-401: A list holding the numbers 1 , 2 , and 3 , usually written as (1 2 3) , might be represented as follows: The memory cells 3 to 5 do not belong to our list, the cells of which can be distributed randomly over the memory. Cell 2 is the head of the list, it points to cell 1, which holds the first element's value, and the list containing only 2 and 3 (beginning at cell 6). Cell 6 points at

348-447: A new value in the PC. These include branches (sometimes called jumps), subroutine calls, and returns . A transfer that is conditional on the truth of some assertion lets the computer follow a different sequence under different conditions. A branch provides that the next instruction is fetched from elsewhere in memory. A subroutine call not only branches but saves the preceding contents of

406-626: A postcard: Dear Professor Church, Russell had the iota operator , Hilbert had the epsilon operator . Why did you choose lambda for your operator? According to Scott, Church's entire response consisted of returning the postcard with the following annotation: " eeny, meeny, miny, moe ". Computable functions are a fundamental concept within computer science and mathematics. The lambda calculus provides simple semantics for computation which are useful for formally studying properties of computation. The lambda calculus incorporates two simplifications that make its semantics simple. The first simplification

464-426: A single input. For example, can be reworked into This method, known as currying , transforms a function that takes multiple arguments into a chain of functions each with a single argument. Function application of the s q u a r e _ s u m {\textstyle \operatorname {square\_sum} } function to the arguments (5, 2), yields at once whereas evaluation of

522-460: A variable living on the outer function's stack. If the nested function were returned from the outer function, then it would be referring to a variable in a stack frame that is no longer present. Turner notes that Landin's SECD machine solves this problem (thus allowing functions to return functions), as a function value is now represented with a closure on the heap that can store the environment of variables it should use irrespective of what happens on

580-480: A variable that has not been bound, such as the term λ x . ( x + y ) {\displaystyle \lambda x.(x+y)} (which represents the function definition f ( x ) = x + y {\displaystyle f(x)=x+y} ). In this term, the variable y has not been defined and is considered an unknown. The abstraction λ x . ( x + y ) {\displaystyle \lambda x.(x+y)}

638-523: Is Turing complete , that is, it is a universal model of computation that can be used to simulate any Turing machine . Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function . Lambda calculus may be untyped or typed . In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are weaker than

SECTION 10

#1732786556955

696-625: Is alpha equivalence . It captures the intuition that the particular choice of a bound variable, in an abstraction, does not (usually) matter. For instance, λ x . x {\displaystyle \lambda x.x} and λ y . y {\displaystyle \lambda y.y} are alpha-equivalent lambda terms, and they both represent the same function (the identity function). The terms x {\displaystyle x} and y {\displaystyle y} are not alpha-equivalent, because they are not bound in an abstraction. In many presentations, it

754-598: Is M applied to N, where M {\displaystyle M} is the lambda term ( λ x . ( λ x . x ) ) {\displaystyle (\lambda x.(\lambda x.x))} being applied to the input N {\displaystyle N} which is x {\displaystyle x} . Both examples 1 and 2 would evaluate to the identity function λ x . x {\displaystyle \lambda x.x} . In lambda calculus, functions are taken to be ' first class values ', so functions may be used as

812-423: Is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution . Untyped lambda calculus, the topic of this article, is a universal model of computation that can be used to simulate any Turing machine (and vice versa). It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into

870-611: Is a lambda term. That is, a lambda term is valid if and only if it can be obtained by repeated application of these three rules. For convenience, some parentheses can be omitted when writing a lambda term. For example, the outermost parentheses are usually not written. See § Notation , below, for an explicit description of which parentheses are optional. It is also common to extend the syntax presented here with additional operations, which allows making sense of terms such as λ x . x 2 . {\displaystyle \lambda x.x^{2}.} The focus of this article

928-595: Is a placeholder in both examples. Here, example 1 defines a function λ x . B {\displaystyle \lambda x.B} , where B {\displaystyle B} is ( λ x . x ) x {\displaystyle (\lambda x.x)x} , an anonymous function ( λ x . x ) {\displaystyle (\lambda x.x)} , with input x {\displaystyle x} ; while example 2, M {\displaystyle M}   N {\displaystyle N} ,

986-413: Is a syntactically valid term and represents a function that adds its input to the yet-unknown y . Parentheses may be used and might be needed to disambiguate terms. For example, The examples 1 and 2 denote different terms, differing only in where the parentheses are placed. They have different meanings: example 1 is a function definition, while example 2 is a function application. The lambda variable x

1044-468: Is also a current research topic in category theory . Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics . The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox . Subsequently, in 1936 Church isolated and published just

1102-514: Is an abstraction representing the function f {\displaystyle f} defined by f ( x ) = x 2 + 2 , {\displaystyle f(x)=x^{2}+2,} using the term x 2 + 2 {\displaystyle x^{2}+2} for t . The name f {\displaystyle f} is superfluous when using abstraction. The syntax ( λ x . t ) {\displaystyle (\lambda x.t)} binds

1160-426: Is available as long as there is a single free memory cell. Even when all cells have been used, garbage collection may yield additional free memory. Obviously, specific implementations of the SECD structure can implement the stack as a canonical stack structure, thus improving the overall efficiency of the virtual machine, provided that a strict bound be put on the dimension of the stack. The C register points at

1218-426: Is execute a usually linear sequence of instructions. Such a PC is central to the von Neumann architecture . Thus programmers write a sequential control flow even for algorithms that do not have to be sequential. The resulting “ von Neumann bottleneck ” led to research into parallel computing , including non-von Neumann or dataflow models that did not use a PC; for example, rather than specifying sequential steps,

SECTION 20

#1732786556955

1276-401: Is indicated by C being empty, in which case the result will be on the stack S . The last saved evaluation state on D is then popped, and the result of the completed evaluation is pushed onto the stack contents restored from D . Evaluation of the restored state then continues as above. If C and D are both empty, overall evaluation has completed with the result on

1334-456: Is no longer required as there will be no name collisions. If repeated application of the reduction steps eventually terminates, then by the Church–Rosser theorem it will produce a β-normal form . Variable names are not needed if using a universal lambda function, such as Iota and Jot , which can create any function behavior by calling it on itself in various combinations. Lambda calculus

1392-492: Is not in the free variables of r {\displaystyle r} ) is crucial in order to ensure that substitution does not change the meaning of functions. Program counter The program counter ( PC ), commonly called the instruction pointer ( IP ) in Intel x86 and Itanium microprocessors , and sometimes called the instruction address register ( IAR ), the instruction counter , or just part of

1450-460: Is simply mapped to itself. The second simplification is that the lambda calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the s q u a r e _ s u m {\textstyle \operatorname {square\_sum} } function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts

1508-401: Is that the lambda calculus treats functions "anonymously;" it does not give them explicit names. For example, the function can be rewritten in anonymous form as (which is read as "a tuple of x and y is mapped to x 2 + y 2 {\textstyle x^{2}+y^{2}} "). Similarly, the function can be rewritten in anonymous form as where the input

1566-416: Is the case with the conventional machines. The current variable environment is managed by the E register, which points at a list of lists. Each individual list represents one environment level: the parameters of the current function are in the head of the list, variables that are free in the current function, but bound by a surrounding function, are in other elements of E . The dump, at whose head

1624-441: Is the pure lambda calculus without extensions, but lambda terms extended with arithmetic operations are used for explanatory purposes. An abstraction λ x . t {\displaystyle \lambda x.t} denotes an § anonymous function that takes a single input x and returns t . For example, λ x . ( x 2 + 2 ) {\displaystyle \lambda x.(x^{2}+2)}

1682-448: Is usual to identify alpha-equivalent lambda terms. The following definitions are necessary in order to be able to define β-reduction: The free variables of a term are those variables not bound by an abstraction. The set of free variables of an expression is defined inductively: For example, the lambda term representing the identity λ x . x {\displaystyle \lambda x.x} has no free variables, but

1740-449: The D register points, is used as temporary storage for values of the other registers, for example during function calls. It can be likened to the return stack of other machines. The memory organization of the SECD machine is similar to the model used by most functional language interpreters : a number of memory cells, each of which can hold either an atom (a simple value, for example 13 ), or represent an empty or non-empty list. In

1798-414: The foundations of mathematics . In 1936, Church found a formulation which was logically consistent , and documented it in 1940. Lambda calculus consists of constructing lambda terms and performing reduction operations on them. In the simplest form of lambda calculus, terms are built using only the following rules: The reduction operations include: If De Bruijn indexing is used, then α-conversion

SECD machine - Misplaced Pages Continue

1856-456: The CPU may compute some other value and load it into the PC by a pulse to its LOAD input. To identify the current instruction, the PC may be combined with other registers that identify a segment or page . This approach permits a PC with fewer bits by assuming that most memory units of interest are within the current vicinity. Use of a PC that normally increments assumes that what a computer does

1914-453: The CPU places the value of the PC on the address bus to send it to the memory. The memory responds by sending the contents of that memory location on the data bus . (This is the stored-program computer model, in which a single memory space contains both executable instructions and ordinary data. ) Following the fetch, the CPU proceeds to execution , taking some action based on the memory contents that it obtained. At some point in this cycle,

1972-412: The PC somewhere. A return retrieves the saved contents of the PC and places it back in the PC, resuming sequential execution with the instruction following the subroutine call. In a simple central processing unit (CPU), the PC is a digital counter (which is the origin of the term "program counter") that may be one of several hardware registers . The instruction cycle begins with a fetch , in which

2030-413: The PC will be modified so that the next instruction executed is a different one (typically, incremented so that the next instruction is the one starting at the memory address immediately following the last memory location of the current instruction). Like other processor registers, the PC may be a bank of binary latches, each one representing one bit of the value of the PC. The number of bits (the width of

2088-463: The PC) relates to the processor architecture. For instance, a “32-bit” CPU may use 32 bits to be able to address 2 units of memory. On some processors, the width of the program counter instead depends on the addressable memory; for example, some AVR microcontrollers have a PC which wraps around after 12 bits. If the PC is a binary counter, it may increment when a pulse is applied to its COUNT UP input, or

2146-518: The SECD machine has been used as the target for other systems such as Lisp/370. In 1989 researchers at the University of Calgary worked on a hardware implementation of the machine. D. A. Turner (2012) points out that the ALGOL 60 programming language could not return functions from other functions (rendering functions no longer first-class). A function nested inside another function could refer to

2204-417: The current contents of S , E , and C are pushed onto the dump D (which is a stack of these triples), S is reinitialized to empty, and C is reinitialized to the application result with E containing the environment for the free variables of this expression, augmented with the binding that resulted from the application. Evaluation then proceeds as above. Completed evaluation

2262-410: The curried version requires one more step to arrive at the same result. The lambda calculus consists of a language of lambda terms , that are defined by a certain formal syntax, and a set of transformation rules for manipulating the lambda terms. These transformation rules can be viewed as an equational theory or as an operational definition . As described above, having no names, all functions in

2320-454: The desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus. Lambda calculus has applications in many different areas in mathematics , philosophy , linguistics , and computer science . Lambda calculus has played an important role in the development of the theory of programming languages . Functional programming languages implement lambda calculus. Lambda calculus

2378-399: The first item in C is a value, it is pushed onto the stack S . More exactly, if the item is an identifier, the value pushed onto the stack will be the binding for that identifier in the current environment E . If the item is an abstraction, a closure is constructed to preserve the bindings of its free variables (which are in E ), and it is this closure which is pushed onto

SECD machine - Misplaced Pages Continue

2436-763: The function λ x . y {\displaystyle \lambda x.y} x {\displaystyle x} has a single free variable, y {\displaystyle y} . Suppose t {\displaystyle t} , s {\displaystyle s} and r {\displaystyle r} are lambda terms, and x {\displaystyle x} and y {\displaystyle y} are variables. The notation t [ x := r ] {\displaystyle t[x:=r]} indicates substitution of r {\displaystyle r} for x {\displaystyle x} in t {\displaystyle t} in

2494-568: The function that always returns y {\displaystyle y} , no matter the input. As an example of a function operating on functions, the function composition can be defined as λ f . λ g . λ x . ( f ( g x ) ) {\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))} . There are several notions of "equivalence" and "reduction" that allow lambda terms to be "reduced" to "equivalent" lambda terms. A basic form of equivalence, definable on lambda terms,

2552-402: The head of the code or instruction list that will be evaluated. Once the instruction there has been executed, the C is pointed at the next instruction in the list—it is similar to an instruction pointer (or program counter ) in conventional machines, except that subsequent instructions are always specified during execution and are not by default contained in subsequent memory locations, as

2610-415: The high-level programmer might specify desired function and the low-level programmer might specify this using combinatory logic . This research also led to ways to making conventional, PC-based, CPUs run faster, including: Modern high-level programming languages still follow the sequential-execution model and, indeed, a common way of identifying programming errors is with a “procedure execution” in which

2668-476: The inputs, or be returned as outputs from other functions. For example, the lambda term λ x . x {\displaystyle \lambda x.x} represents the identity function , x ↦ x {\displaystyle x\mapsto x} . Further, λ x . y {\displaystyle \lambda x.y} represents the constant function x ↦ y {\displaystyle x\mapsto y} ,

2726-415: The instruction sequencer, is a processor register that indicates where a computer is in its program sequence. Usually, the PC is incremented after fetching an instruction , and holds the memory address of (" points to") the next instruction that would be executed. Processors usually fetch instructions sequentially from memory, but control transfer instructions change the sequence by placing

2784-549: The lambda calculus are anonymous functions. They only accept one input variable, so currying is used to implement functions of several variables. The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid C programs and some are not. A valid lambda calculus expression is called a " lambda term ". The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms: Nothing else

2842-471: The latter case, the cell holds two pointers to other cells, one representing the first element, the other representing the list except for the first element. The two pointers are traditionally named car and cdr respectively—but the more modern terms head and tail are often used instead. The different types of values that a cell can hold are distinguished by a tag . Often different types of atoms (integers, strings, etc.) are distinguished as well. So,

2900-402: The portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus . Until the 1960s when its relation to programming languages was clarified, the lambda calculus was only a formalism. Thanks to Richard Montague and other linguists' applications in

2958-410: The semantics of natural language, the lambda calculus has begun to enjoy a respectable place in both linguistics and computer science. There is some uncertainty over the reason for Church's use of the Greek letter lambda (λ) as the notation for function-abstraction in the lambda calculus, perhaps in part due to conflicting explanations by Church himself. According to Cardone and Hindley (2006): By

SECTION 50

#1732786556955

3016-425: The stack S . The SECD machine is stack-based . Functions take their arguments from the stack. The arguments to built-in instructions are encoded immediately after them in the instruction stream. Like all internal data-structures, the stack is a list, with the S register pointing at the list's head or beginning. Due to the list structure, the stack need not be a continuous block of memory, so stack space

3074-420: The stack. If the item is ap , two values are popped off the stack and the application done (first applied to second). If the result of the application is a value, it is pushed onto the stack. If the application is of an abstraction to a value, however, it will result in a lambda calculus expression that may itself be an application (rather than a value), and so cannot be pushed onto the stack. In this case,

3132-496: The stack. When evaluation of an expression begins, the expression is loaded as the only element of control C . The environment E , stack S and dump D begin empty. During evaluation of C it is converted to reverse Polish notation (RPN) with ap (for apply ) being the only operator. For example, the expression F (G X) (a single list element) is changed to the list X:G:ap:F:ap . Evaluation of C proceeds similarly to other RPN expressions. If

3190-520: The untyped lambda calculus, which is the primary subject of this article, in the sense that typed lambda calculi can express less than the untyped calculus can. On the other hand, typed lambda calculi allow more things to be proven. For example, in simply typed lambda calculus , it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate (see below ). One reason there are many different typed lambda calculi has been

3248-489: The variable x in the term t . The definition of a function with an abstraction merely "sets up" the function but does not invoke it. An application t {\displaystyle t}   s {\displaystyle s} represents the application of a function t to an input s , that is, it represents the act of calling function t on input s to produce t ( s ) {\displaystyle t(s)} . A lambda term may refer to

3306-637: The way, why did Church choose the notation “λ”? In [an unpublished 1964 letter to Harald Dickson] he stated clearly that it came from the notation “ x ^ {\displaystyle {\hat {x}}} ” used for class-abstraction by Whitehead and Russell , by first modifying “ x ^ {\displaystyle {\hat {x}}} ” to “ ∧ x {\displaystyle \land x} ” to distinguish function-abstraction from class-abstraction, and then changing “ ∧ {\displaystyle \land } ” to “λ” for ease of printing. This origin

3364-454: Was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and λ just happened to be chosen. Dana Scott has also addressed this question in various public lectures. Scott recounts that he once posed a question about the origin of the lambda symbol to Church's former student and son-in-law John W. Addison Jr., who then wrote his father-in-law

#954045