lambda ..

[Francois-Rene Rideau]

On Wed, Oct 21, 1998 at 08:42:27AM -0700, Tril wrote:
> A lambda abstraction implicitly defines half of a substitution operation.
> The lambda application defines the other half of what is needed to
> complete substitution but still the fact that substitution is taking place
> is implicit, in the lambda syntax.
This is why lambda-calculi with explicit substitutions were invented,
the most well-known of which being the lambda-sigma calculus
(see $TUNES/src/HLL/scm/lambda-foo.scm for a description).
Though the formalization as a finite presentation in rewrite logic
dates only back to the early 80s (See things by Lévy, Hall, Abadi, etc).
The original idea can be traced back to deBruijn in the 60s(?).

> This is unacceptable.  Every operation must be explicit. How do you
> implement lambda calculus using lambda calculus?
Papers by Jean Goubault http://hypatia.dcs.qmw.ac.uk/authors/G/GoubaultJ/
use it for a "reflective" lambda-eval-quote-calculus that maps modal logic
just like lambda-calculus mapped logic thru the Curry-Howard isomorphism.

> What if I want
> abstractions to implicitly define other operations besides substitution?
I'm not sure what you hereby mean by "abstraction".

> If you can abstract ANY property, as you said in the web pages, Fare, why
> must every property conform to a low-level "Search and replace" paradigm
> of lambda?
We should certainly be able to express other properties than lambdas.
It's just that lambda (or rather, lambda-eval-quote) constitutes a minimal
reflective logic with well-defined operational semantics (i.e. implementable),
out of which we may build the rest.

> Sure, maybe it's "complete" and therefore possible... that
> doesn't mean it's easy for the programmer to do.
We'll certainly have to build a lot over that core before the programmer
is enabled to use a "purely declarative" programming style.

## Faré | VN: Уng-Vû Bân   | Join the TUNES project!  http://www.tunes.org/ ##
## FR: François-René Rideau |    TUNES is a Useful, Not Expedient System     ##
## Reflection&Cybernethics  | Project for a Free Reflective Computing System ##
The rule is, jam to-morrow and jam yesterday, but never jam today.
                -- Lewis Carroll