lambda ..

[RE01 Rice Brian T. EM2]

>> 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(?).
hmm.
>> 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.
ok. now that i've thought about it, that research will be pretty useful.
>> 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.
good enough for me. as far as i'm concerned, the argument is on hold.
let's discuss what sort of lambda(based)-calculus implementation we can
work with, with the goal of other-language generation being the limit of
the project.  i'm still very concerned about the limits of this
approach, but practicality is the most important measure we have right
now.
>> 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.
let's do that.