3 ms·
If you define true and false as abstractions: true ::= \x\y,x false ::= \x\y,y Then the conditional comes for free, since it is an application of true
by PartiallyTyped 3y ago
If you define true and false as abstractions:
true ::= \x\y,x
false ::= \x\y,y
Then the conditional comes for free, since it is an application of true. You can define not as
not ::= \b, b false true
You can then define 'and' as
and ::= \x\y, x y false
- cvoss 3y agoThat won't work in simply typed lambda calculus. (Try to write down the types involved!) Either untyped or dependently typed is required.
- PartiallyTyped 3y agoI have to admit that I am out of my field, so help me a bit, you expressed that it must be dependently typed because false and true are a -> b -> a|b under union (and a->b->b and a->b->a respectively) so the the abstractions can take any functions subtyping a->b->a|b, thus to make them correct you need dependent types to verify that the abstractions take only True and False? Is this correct?
- cvoss 3y agoThe only types available to you in this flavor of STLC are bool, bool -> bool, bool -> bool -> bool, (bool -> bool) -> bool, etc. Structurally, if `true := \x\y.x`, the simplest attempt at typing it would be `true : bool -> bool -> bool`. But that means `true` can't have type `bool`! What you need is to say that true (like false) chooses one of its two inputs to return, no matter what type that happens to be. So we introduce a type parameter (think Java generics, if that's what you're familiar with). "Given any type T, `true T` has type T -> T -> T". A formalized notation for this (there is more than one notation you'll see) is `true : ∀ (T : Type), T -> T -> T`. And `false` has the same type. This type obviates the need for a declared `bool` type.