Friday, June 21, 2013

Let’s go skiing

Can’t be enacted with only one vote… — Quirck

Adminned at 23 Jun 2013 14:11:19 UTC

Axioms:

* S, K, I, B, C, K, and W are Expors.
* For all Expors x and y, x y is an Expor.
* For all x, $(x) is an Expor, and $’($(x)) = x.
* For all Expors x and y, if [for all Expors z, (x z) = (y z)], then x = y.
* For all Expors x, y and z, ((S x) y) z = (x z) (y z).
* For all Expors x and y, (K x) y = x.
* For all Expors x, I x = x.
* For all Expors x, y and z, ((B x) y) z = x (y z).
* For all Expors x, y and z, ((C x) y) z = (x z) y.
* For all Expors x and y, (W x) y = (x y) y.

See http://en.wikipedia.org/wiki/SKI_combinator_calculus and http://en.wikipedia.org/wiki/B,C,K,W_system. Irreducible Expors, like ((S I) I) ((S I) I), aren’t a problem; they are simply undefined. The only way you could prove a paradox from these axioms is by proving that $(x) = $(y) where x ≠ y, and I’m pretty sure you can’t do that, because it’s impossible for two combinator calculus terms to have substantively different reductions,

Comments

Skju:

06-22-2013 03:31:34 UTC

Why have both systems?

Tavros:

06-22-2013 20:53:02 UTC

Uh, good question. I wasn’t really thinking about that, I guess,