Fw: Technical theoretical question about lazy evaluation

Maarten Maartensz maartens at xs4all.nl
Mon Dec 27 10:48:33 UTC 2004


----- Original Message ----- 
From: "Maarten Maartensz" <maartens at xs4all.nl>
To: <squeak-dev at lists.squeakfoundation.org>
Sent: Monday, December 27, 2004 11:44 AM
Subject: Technical theoretical question about lazy evaluation


> Hello,
>
> Being a person of a theoretical bend I have a technical theoretical question
I'd
> like to have references about, to material preferably on the internet
somewhere,
> that relates to the following quotation (and please don't read on if you don't
> care for abstruse technicalities) of part of a paragraph by Per-Martin Löf, in
> his "Constructive Mathematics and Computer Programming", which is in "Logic,
> Methodology and Philosophy of Science VI", of 1982.
>
> Note: The '|' symbol stands for the lambda in what follows:
>
> "When variable binding forms of expression are introduced, as they are in the
> theory of types, it is no longer possible, in general, to evaluate the
> expresssions from within. To evaluate (|x)b, for example, we should first have
> to evaluate b. But b cannot be evaluated, in general, until a value has been
> assigned to the variable x. In the theory of types, this difficulty has been
> overcome by reversing the order of evaluation: instead of evaluating the
> expressions from within, they are evaluated from without. This is known as
head
> reduction in combinatory logic and normal order or lazy evaluation in
> prograrmming. For example (|x)b is simply assigned itself as value. (...) What
> is significant, though, is that the principle of Frege's referred to above,
> namely that the value of an expression depends only on the values of its
parts,
> is irretrievably lost. To make the language work in spite of this loss has
been
> one of the most serious difficulties in the design of the theory of types."
(p.
> 160-1)
>
> If you're still around here: I'd like references to the problem indicated by
> Martin-Löf's
>
> "What is significant, though, is that the principle of Frege's referred to
> above, namely that the value of an expression depends only on the values of
its
> parts, is irretrievably lost."
>
> and the more these references have to do with mathematical logic the better it
> is, from my own point of view. What I'd most like to see, indeed, are
references
> to texts that systematically and logically deal with model-theoretical
semantics
> and the loss of Frege's principle of the compositionality of meaning.
>
> Since lazy evaluation is so important for the foundation of Smalltalk and
> Squeak, it seems this list is one place to ask.
>
> Thanks for your help.
>
> Regards,
>
> Maarten.
> ---------------------------------------
> Maarten Maartensz. Homepage:
> http://www.maartensz.org
> ---------------------------------------
>





More information about the Squeak-dev mailing list