@MSGID:
<60e0a8b6-18e4-4b10-83e5-b32ea7e30c06n@googlegroups.com> 18384b58
@REPLY: <875ygfcnb1.fsf@bsb.me.uk> 0ad1db41
@REPLYADDR Rock Brentwood
<rockbrentwood@gmail.com>
@REPLYTO 2:5075/128 Rock Brentwood
@CHRS: CP866 2
@RFC: 1 0
@RFC-References:
<cba4f733-5232-4ec4-9a16-ff5828e84b8cn@googlegroups.com> <cc7dff2c-dbdd-4888-ba71-3c122993fd01n@googlegroups.com>
<875ygfcnb1.fsf@bsb.me.uk>
@RFC-Message-ID:
<60e0a8b6-18e4-4b10-83e5-b32ea7e30c06n@googlegroups.com>
@TZUTC: -0700
@PID: G2/1.0
@TID: FIDOGATE-5.12-ge4e8b94
On Wednesday, October 19, 2022 at 8:10:31 PM UTC-5, Ben Bacarisse wrote:
> Hey! A topical post!
> > Lambda Calculus with infinitary terms (and the conditional operator). 
> > Notation: x = A, B means (lambda x B) A
> Curious notation. Is it your own? Presumably 
> 
> x=A, y=B, C 
> 
> means 
> 
> (lambda x ((lambda y C) B)) A 

 ... which is all it can mean, since x = A, y = B, C means x =
A, (y = B, C), and x = a, f (which is often written as "let x =
a in f") stands for (lxf)a ... which is standard notation, in case
you forgot. It`s just a more natural abbreviated form of it, without
the "let" or "in" as you (presumably) already know.

So x = A, (y = B, C) mean x = A, ((lyC) B) means lx((lyC)B)A.
> rather than the more usual 

No. There is no "more usual".
let x = A in let y = B in C means lx((lyC)B)A.

> This raises the question of how you write 
> 
> (lambda x (lambda y C)) A B 

the same way as you always do:
(lx(lyC))BA
or equivalently as
(x = B, lyC)A
which (in the less abbreviated form) is
(let x = B in lyC)A

Perhaps you missed the part up at the top where it said:
> Lambda Calculus *with* infinitary terms
that means *extension of* not *replacement for*.

> I`m not seeing the advantages of this notation. 

 An upward extension of a given language is *always* more useful or
"advantageous" than the language it extends - almost by definition of "useful" ...
provided the language, itself, has the same meaning (and parsing) in the
extension as it does in the original ... since it includes the original
language, itself, and adds more. That`s universally true, regardless of the
context or situation and independently of how "useful" or "advantage" is
defined.
--- G2/1.0
 * Origin: usenet.network (2:5075/128)
SEEN-BY: 5001/100 5015/255 5019/40 5020/715 848
1042 4441 12000 5030/49 1081
SEEN-BY: 5058/104 5075/128
@PATH: 5075/128 5020/1042 4441