A Formulation of Lambda Calculus with Variables without Substitution

[rockbr...@gmail.com]

The approach adopted by DeBruijn is fairly well-known: to eliminate the
variables and avoid the difficulties with free and bound variables and
the like; or to replace the Lambda Calculus by the use of combinators.
Otherwise, to get a fully formalized self-contained Lambda Calculus,
one needs to include an explicit substitution operation -- or so it is
assumed.

But, in fact, there is a quick and easy way out, taking advantage of
the Beta Rule itself which essentially gives you an *internal*
definition of substitution!

As a result, the clauses that would normally be issued to define a
formalized substitution operator become the basic reduction rules.
Moreover, under this revision, the alpha rule becomes a special case of
the eta rule.

Let (x = U, T) denote the substitution of term U for variable x in T.
This operation can be formally defined by the clauses:
sigma_I: (x = U, x) = x
sigma_K: (y = U, T) = T if y does not occur freely in T
sigma_S: (x = U, T T') = (x = U, T) (x = U, T')
sigma_lambda: (x = U, lambda y.T) = lambda y.(x = U, T),
if y is distinct from x and does not occur freely in U.

The alpha, beta and eta rules are:
alpha: lambda x.T = lambda y.(x = y, T),
where y does not occur freely in T

beta: (lambda x.T) U = (x = U, T)

eta: lambda y.Ty = T, where y does not occur freely in T

Taking beta as a definition and applying that definition to (sigma_I,
sigma_K, sigma_S, sigma_lambda, alpha, eta) results respectively in the
following rules
beta_I: (lambda x.x)U = x
beta_K: (lambda y.T)U = T, if y does not occur freely in T
beta_S: (lambda x.T T')U = ((lambda x.T) U) ((lambda x.T') U)
beta_lambda: (lambda x.(lambda y.T))U = lambda y.((lambda x.T) U),
if y is distinct from x and does not occur freely in U

beta_alpha: lambda x.T = lambda y.((lambda x.T) y),
if y does not occur freely in T

eta: lambda y.Ty = T, where y does not occur freely in T.

The first five rules suffice to characterize the lambda calculus
without the eta rule, while the replacement of beta_alpha by its
generalization eta suffices to characterize the lambda calculus with
the eta rule.

Unlike the beta rule, none of these "beta" rules involve the
substitution operator (x = U, T). Instead, they are all combinatorial
-- but with variables, not combinators!

[rockbr...@gmail.com]

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.