# Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings

Authors
Publication Date
Source
Legacy

## Abstract

MATHEMATICS Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings Dedicated to A. Heyting at the occasion of his 80th birthday on May 9,1978 Communicated at the meeting of March 18, 1978 Department of Mathematics, Eindhoven University of Technology, The Netherlands 1. INTRODUCTION ON NAME-CARRYING LAWBDA CALCULUS In ordinary lambda calculus we use names both for free and for bound variables. Let us present an example that explains what kind of expressions we are after: apart from names for variables we have names for constants. We may have introduced an expression in two variables x and y, and have abbreviated it to f(x, y) (now f is the "constant" we mentioned). Now 3LZf(x, y) is a lambda expression. Its interpretation is: the function that attaches to every x the value f(x, y). The letter y is a free variable and x a bound variable in the expression il,f(x, y). We can, of course, also write more complex lambda expressions like In this example the free variables are y and s. Usual lambda calculus has a notation (in the form of concatenation) for "application" that intends to express "the value of the function y a t the point x". We do not need a special notation for this, because we can devote a special constant A to this purpose, and write that value as A(y, x). Now so-called beta-reduction is a kind of elimination of such an A, like the passage from A(&(/ (x, y)), g(t)) to f(g(t), y). The latter two formulas are not considered to be equal (in spite of their common inter- pretation). On the other hand, the difference between W(x, y) and Reprinted from Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, Amsterdam, series A, volume 81 (3), September 22, 1978 L,f(u, y) is much less essential. The desire to identify them lies a t the root of namefree lambda calculus. The kind of name-carrying lambda calculus described above is exactly the same as in [I]. We close this se

Seen <100 times