CS puzzle

[bitwiseshiftleft]

OK, this is both a logic puzzle (in the sense that it's about logic) and a CS puzzle, so I'm not sure where it belongs, but here goes.

The Curry-Howard isomorphism says, roughly, that logic is the same as type systems, and that proofs are the same as programs.

The usual form is that !x is a [k]ontinuation taking an x, x&y is a pair, x|y is a disjunction (a variable which is Either an x or a y), and x -> y is a function from x to y. P == Q (two formulas are equivalent) is the same as saying (P -> Q) & (Q -> P).

So for instance, a&b -> a is the type of λ(a,b) . a (also known as fst); a -> (b -> a) is the type of const, a -> a|b is the type of L (or Left), a -> (b -> (a&b)) is the type of curry id, and so on.

As a slightly trickier example, we can write out DeMorgan's laws (in some sort of hacked-up lambda calculus notation):

!(a|b) -> !a & !b is
λk . (λx . k (L x), λx . k (R x))
= λk . (k∘L, k∘R)

and the reverse, !a & !b -> !(a|b), is
λ(ka,kb) . either ka kb
= uncurry either

Similarly !a|!b -> !(a&b) is
either (λk . λ(x,y) . k x) (λk . λ(x,y) . k y)
= either (∘fst) (∘snd)

So what, then, is a program which proves
!(a & b) -> !a | !b

?

[iw]

It's clear that this is Haskell-inspired, but your terms are still pretty confusing. Could you explain them a little further? (makes it seem a homework problem )

If I had to guess, tho:

λk . either (λx . fst (k x))((λx . snd (k x))

[adlaiff6]

I too wish I understood all those terms.

[iw]

I thought about this a bit more, and couldn't you just do stuff like:

a & b -> a | b
λ(a,b) . either a b

a | b -> a & b
λab -> (L ab, R ab)

to show that a&b == a|b ? I don't know if I get what's going on here.

I also don't think I understand what you mean by [k]ontinuation. I thought "!a" was the same as "λk . a" but now I dunno. I should mention I don't have very much knowledge of the lambda calculus.

I'm gonna go read the (difficult-looking) Wikipedia page on Curry-Howard...

[bitwiseshiftleft]

Er. So yeah, sorry to be confusing. This isn't actually Haskell-inspired, but rather CS-theory-inspired.

A continuation is a function (in the programming sense, not in the strict mathematical sense) that takes some value and doesn't ever return. They're used a lot in Scheme. They're usually written k, which is why I said [k]ontinuation. So if you say that not returning is like "false", a continuation taking an x has type x->False, which is to say, !x (the ! means not here, since I was too lazy to find the unicode negation sign).

Either is a library function in a lot of functional languages. It takes a function taking an x, a function taking a y, and an x|y, and then invokes the appropriate one. It has type (x->z) -> (y->z) -> (x|y) -> z, which is a pretty obvious logical statement. I'm taking it as a primitive, because I haven't defined another way to extract values from x|y. More on that later.

Fst takes a pair and returns the first element, and so has type (x&y) -> x; similarly, snd is (x&y) -> y.

L and R have types x->x|y and y->x|y, respectively.

∘ (supposed to be the o-shaped "compose" operator, in case there are Unicode issues) composes two functions: f∘g = λx . f (g x). It has type (y->z) -> (x->y) -> (x->z).

You don't want to show that x&y -> x|y, because that's obvious (L∘fst and R∘snd both suffice). Rather, you want to show that !(x&y) -> !x | !y.

I talked to a friend about this the other day; apparently the reason that it's hard to write this function is that usually | is defined as x|y == !(!x&!y), but I'm making it primitive instead (this makes either unnecessary). That means that another function, most likely Scheme's call/cc (of type !!a -> a) is required. As it happens, call/cc expands the Curry-Howard isomorphism from intuitionistic logic to classical logic (I'm not a logic buff, so I'm not sure what the distinction is, other than that in intuitionistic logic !!a doesn't imply a), while the standard definition of | doesn't. I don't know why. Wikipedia probably does.

And no, this isn't homework.

[iw]

It just sounded so out of left field that it almost seemed like a verbatim c&p of a homework assignment.

So am I right in saying that !x is of type (x->Never), for example?
So in:
!a & !b -> !(a|b)
we want ((a->Never), (b->Never)) -> (a|b -> Never).
And the answer is:
λ(ka,kb) . either ka kb
where either is (x->z) -> (y->z) -> (x|y) -> z and since ka and kb are of type (x->Never), we get a function (x|y -> Never). I think I'm with you now.

Am I right in saying that if we had a function "combine" with type x -> y -> x|y, we could just say:
!(a & b) -> !a | !b proved by
λk . combine (λx . k (fst x)) (λx . k (snd x)) ?

[bitwiseshiftleft]

It just sounded so out of left field that it almost seemed like a verbatim c&p of a homework assignment.

So am I right in saying that !x is of type (x->Never), for example?
So in:
!a & !b -> !(a|b)
we want ((a->Never), (b->Never)) -> (a|b -> Never).
And the answer is:
λ(ka,kb) . either ka kb
where either is (x->z) -> (y->z) -> (x|y) -> z and since ka and kb are of type (x->Never), we get a function (x|y -> Never). I think I'm with you now.

Yes, exactly.

Am I right in saying that if we had a function "combine" with type x -> y -> x|y, we could just say:
!(a & b) -> !a | !b proved by
λk . combine (λx . k (fst x)) (λx . k (snd x)) ?

No, the problem is that fst has type (a&b) -> a, not a -> (a&b). (As for combine, there are two obvious functions with type x -> y -> x|y.)

This is sort of like trying to prove (a | !a): you can't just return an L or an R.

[iw]

Next try:
You can show !(a & b) -> ((a & b) -> (!a | !b)) by
λk . λ(x,y) . combine (λz . k (x,z)) (λz . k (z y))

And from there, you prove that ((a & b) -> (!a | !b)) == a! | b!. Or is that totally off?

[bitwiseshiftleft]

Next try:
You can show !(a & b) -> ((a & b) -> (!a | !b)) by
λk . λ(x,y) . combine (λz . k (x,z)) (λz . k (z y))

And from there, you prove that ((a & b) -> (!a | !b)) == a! | b!. Or is that totally off?

Well, it would work, except that I think the second part is just as hard to prove...

You'll need to use call/cc.