Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.

Dismiss

26 views

Skip to first unread message

Aug 12, 2016, 10:03:52 AM8/12/16

to

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!

Aug 14, 2016, 8:13:36 AM8/14/16

to

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.

0 new messages

Search

Clear search

Close search

Google apps

Main menu