On Friday, August 12, 2016 at 9:03:52 AM UTC-5,
rockbr...@gmail.com
wrote:
> Let (x = U, T) denote the substitution of term U for variable x in T.
> sigma_I: (x = U, x) = x
> beta_I: (lambda x.x)U = x
Oops. That should be U on the right-hand side
sigma_I: (x = U, x) = U
beta_I: (lambda x.x)U = U
As far as the approach by combinators goes --- on an additional note: I
actually *did* do a formulation with combinators (with software) a
while back that implemented the eta rule.
However, unlike the usual approach to resolving the problem of the eta
rule, it is not purely equational. To prove SK reduces to KI first
requires adding dummy variables to get SKuv; reducing SKuv -> Kv(uv) ->
v; and then applying an abstraction algorithm lambda u.lambda v.v =
lambda u.I = KI.
A nice axiomatic formulation for eta is difficult to come by and almost
invariably leads one to algebras for category theory.