Abstraction (or, Lambda Calculus for Dummies)

Fare Rideau rideau@nef.ens.fr
Fri, 12 Dec 1997 15:30:45 +0100 (MET)


[-- Note: Can anyone on the list point to any good references about
lambda-calculus? I'd put them on the Review/VMs.html page...
Off hand, I'd recommend Scheme books like SICP for the trivially typed case,
and the caml-light 0.74 tutorial for the structurally typed case.
]


Dear Tril,

> What are the semantics of the abstraction function?
The abstraction is not a function, but a meta-operator,
that takes variables (parameter names), and an expression (the body),
and makes a function that takes arguments, binds the parameters to them,
then evaluate the body in the environment of definition of the function
enriched by these new bindings.

Hence, the function lambda(f,x).f(x) is a function that takes
a pair (f,x) of arguments, then applies function f with argument x,
and returns the result.

> I don't know what a lambda calculus is, and I tried looking at
> the "standard reference" but it didn't make much sense because
> I'm not familiar with set theory or notation.
>
Hum. Anyone knows any good intros to \lambda-calculus on the Web?
[BTW, was the "standard reference" the Barendregt book?]

> In the HLL Semantics page, you give an example of the syntax of
> abstraction:  lambda (x).sin(2*x+1)
>
That's an anonymous function that takes an argument, locally called x
in the function body's scope, and then evaluates to the sine of the sum
of one and the double of x. In OCaml, you would write (dot for float nums/ops)
	fun x -> sin(2. *. x +. 1.)
If numbers need not have a name, and functions have as much rights as
numbers, then it must be possible for functions not to have a name.

> If this is making a new function, shouldn't we give it a name?
You can, by having, (still using OCaml syntax) e.g.
	let f = fun x -> sin(2.*.x+.1.)
much like you can give a name to number 2*10+9 by having
	let twenty_nine = 2*10+9
Of course, you can have special forms handle at the same time naming
and definition of a function, as in
	let double(x) = 2*x

> Something
> like "lambda f(x).sin(2*x+1)"  Or is this just evaluating an expression
> that has 'x' in it?  Is the abstraction function taking x out of the
> expression 2*x+1 or putting it in?
It delays the evaluation of sin(2*x+1) in a environment where x will
be bound to the argument of the function.

> [...] Can you abstract something without creating a new function? [...]
The result of abstracting something *is* by definition a function
having this something as a parameter.

== Faré -=- (FR) François-René Rideau -=- (VN) Уng-Vû Bân -=- rideau@ens.fr ==
Join a project for a free reflective computing system! | 6 rue Augustin Thierry
TUNES is a Useful, Not Expedient System.               | 75019 PARIS     FRANCE
http://www.eleves.ens.fr:8080/home/rideau/Tunes/ -=- Reflection&Cybernethics ==