3.14159265... wrote:What about quantization? we DO live in a integer world?
crp wrote:oh, i thought you meant the entire funtion was f(n) = (-1)^n
i's like girls u crazy
iw wrote: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?
!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)) ?
iw wrote: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?
Users browsing this forum: Exabot [Bot] and 2 guests