|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
> Alan Smaill wrote:
>
>> So the resultant program is
>
>> lambda(~,
>> lambda(~,
>> lambda(~,lambda(v0,lambda(v1,lambda(v2,v0 of v2 of(v1 of v2)))))))
>
>> Here the "~" are used instead of variables where the variable does
>> not appear in the body of the term.
>
>> Are clear about how this program was obtained from the proof?
>> If so, I will go on to answer your questions.
>
> This is not standard lambda calculus syntax.
As I already said:
lambda(v,t) for variable v and term t is lambda abstraction wrt v;
t1 of t2 for terms t1, t2 is application of t1, t2.
> What is the above program
> supposed to be doing -
Are you happy that I have described how to evaluate the terms that arise
up thread?
> what algorithm is it executing?
We have synthesised the S combinator
en.wikipedia.org/wiki/Combinatory_logic
--
Alan Smaill
|
|