Rock Brentwood

2011-10-01 04:10:58 UTC

You read it right: "... WITHOUT Substitution."

So, what's the trick? Answer: treat beta-reduction as a definition,

not as a rule; then, pull back all the clauses that recursively define

substitution through the beta rule into specialized instances of the

beta and eta rules.

The notation here is:

\x.T -- lambda abstraction of x on T.

(x = U, T) -- substitution of U for all free occurrences of x in T.

@T -- the set of variables that freely occur in T.

One should have:

@(x) = {x}, for variables x

@(TT') = @T union @T'

@(\x.T) = @T - {x}

@(x = U, T) = @T, if x is not in @T

@(x = U, T) = (@T - {x}) union @U, if x is in @T,

the last two rules should be derivable from whatever definition is

posed for substitution.

We also use the conventions:

* products associate to the right, e.g. (TU)V = TUV

* lambdas have broader scope, e.g. \x.TU = \x.(TU).

* lambdas compound, e.g. \xyz.T = \x.(\y.(\z.T)).

These are the rules -- treated as equivalences:

alpha: \x.T = \y.(x = y, T), if y is not in @T

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

eta: T = \x.Tx, if x is not in @T.

For substitution, we use the following equivalences:

sigma_I: (x = U, x) = U

sigma_K: (x = U, T) = T, if x is not in @T

sigma_S: (x = U, TT') = (x = U, T) (x = U, T')

sigma_lambda: (x = U, \y.T) = \y.(x = U, T), if y is not in {x} union

@U.

For sigma_lambda, the case y = x is already covered by sigma_K; and

the case where y is in @U, one can still pose an equivalence through

the alpha equivalence:

(x = U, \y.T)

= (x = U, \z.(y = z.T))

= \z.(x = U, (y = z, T))

for any variable z that is not in @T union {x} union @U.

In any case, the sigma rules satisfy the properties asserted for @(x =

U, T).

So ... after treating beta as a definition, applying it to the alpha

and sigma rules to eliminate all the substitutions and then

eliminating the beta equivalence, we get:

* beta_alpha: \x.T = \y.(\x.T)y, if y is not in @T

* eta: T = \x.Tx, if x is not in @T

* beta_I: (\x.x)T = T

* beta_K: (\x.T)U = T, if x is not in @T

* beta_S: (\x.TT')U = (\x.T)U ((\x.T')U)

* beta_lambda: (\x.\y.T)U = \y.(\x.T)U, if y is not in {x} union @U.

Moreover, the beta_alpha rule is a special case of the eta rule, so it

can be eliminated, if the eta rule is used. So, then, even the alpha

rule is eliminated.

Otherwise, if eta is not used, then alpha lives on as the specialized

version of eta: beta_alpha.

Notice, also, how, when the equivalences are read as rules, that the

non-determinism of sigma_lambda (which occurs when we need to go

through the alpha rule when y is in @U) is mostly eliminated and

isolated to the beta_alpha rule or more generally to the eta rule.

Either way, I don't think the conversion from sigma to beta affects

confluence properties, though this needs to be checked closely.

EXAMPLE:

Let S = \xyz.xz(yz), K = \xy.x, I = \x.x, and assume that x, y and z

name distinct variables.

Then

SK = (\xyz.xz(yz)) K

= \y.(\xz.xz(yz))K, by beta_lambda

= \yz.(\x.xz(yz))K, by beta_lambda

= \yz.(\x.xz)K ((\x.yz)K), by beta_S

= \yz.(\x.xz)K (yz), by beta_K

= \yz.(\x.x)K ((\x.z)K) (yz), by beta_S

= \yz.(\x.x)(\xy.x) z(yz), by beta_K

= \yz.(\xy.x) z (yz), by beta_I

= \yz.(\y.(\x.x)z) (yz), by beta_lambda

= \yz.(\y.z) (yz), by beta_I

= \yz.z, by beta_K.

KI = (\xy.x)(\x.x)

= \y.(\x.x)(\x.x), by beta_lambda

= \y.\x.x, by beta_I

= \yz.(\x.x)z, by beta_alpha

= \yz.z, by beta_I

So, what's the trick? Answer: treat beta-reduction as a definition,

not as a rule; then, pull back all the clauses that recursively define

substitution through the beta rule into specialized instances of the

beta and eta rules.

The notation here is:

\x.T -- lambda abstraction of x on T.

(x = U, T) -- substitution of U for all free occurrences of x in T.

@T -- the set of variables that freely occur in T.

One should have:

@(x) = {x}, for variables x

@(TT') = @T union @T'

@(\x.T) = @T - {x}

@(x = U, T) = @T, if x is not in @T

@(x = U, T) = (@T - {x}) union @U, if x is in @T,

the last two rules should be derivable from whatever definition is

posed for substitution.

We also use the conventions:

* products associate to the right, e.g. (TU)V = TUV

* lambdas have broader scope, e.g. \x.TU = \x.(TU).

* lambdas compound, e.g. \xyz.T = \x.(\y.(\z.T)).

These are the rules -- treated as equivalences:

alpha: \x.T = \y.(x = y, T), if y is not in @T

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

eta: T = \x.Tx, if x is not in @T.

For substitution, we use the following equivalences:

sigma_I: (x = U, x) = U

sigma_K: (x = U, T) = T, if x is not in @T

sigma_S: (x = U, TT') = (x = U, T) (x = U, T')

sigma_lambda: (x = U, \y.T) = \y.(x = U, T), if y is not in {x} union

@U.

For sigma_lambda, the case y = x is already covered by sigma_K; and

the case where y is in @U, one can still pose an equivalence through

the alpha equivalence:

(x = U, \y.T)

= (x = U, \z.(y = z.T))

= \z.(x = U, (y = z, T))

for any variable z that is not in @T union {x} union @U.

In any case, the sigma rules satisfy the properties asserted for @(x =

U, T).

So ... after treating beta as a definition, applying it to the alpha

and sigma rules to eliminate all the substitutions and then

eliminating the beta equivalence, we get:

* beta_alpha: \x.T = \y.(\x.T)y, if y is not in @T

* eta: T = \x.Tx, if x is not in @T

* beta_I: (\x.x)T = T

* beta_K: (\x.T)U = T, if x is not in @T

* beta_S: (\x.TT')U = (\x.T)U ((\x.T')U)

* beta_lambda: (\x.\y.T)U = \y.(\x.T)U, if y is not in {x} union @U.

Moreover, the beta_alpha rule is a special case of the eta rule, so it

can be eliminated, if the eta rule is used. So, then, even the alpha

rule is eliminated.

Otherwise, if eta is not used, then alpha lives on as the specialized

version of eta: beta_alpha.

Notice, also, how, when the equivalences are read as rules, that the

non-determinism of sigma_lambda (which occurs when we need to go

through the alpha rule when y is in @U) is mostly eliminated and

isolated to the beta_alpha rule or more generally to the eta rule.

Either way, I don't think the conversion from sigma to beta affects

confluence properties, though this needs to be checked closely.

EXAMPLE:

Let S = \xyz.xz(yz), K = \xy.x, I = \x.x, and assume that x, y and z

name distinct variables.

Then

SK = (\xyz.xz(yz)) K

= \y.(\xz.xz(yz))K, by beta_lambda

= \yz.(\x.xz(yz))K, by beta_lambda

= \yz.(\x.xz)K ((\x.yz)K), by beta_S

= \yz.(\x.xz)K (yz), by beta_K

= \yz.(\x.x)K ((\x.z)K) (yz), by beta_S

= \yz.(\x.x)(\xy.x) z(yz), by beta_K

= \yz.(\xy.x) z (yz), by beta_I

= \yz.(\y.(\x.x)z) (yz), by beta_lambda

= \yz.(\y.z) (yz), by beta_I

= \yz.z, by beta_K.

KI = (\xy.x)(\x.x)

= \y.(\x.x)(\x.x), by beta_lambda

= \y.\x.x, by beta_I

= \yz.(\x.x)z, by beta_alpha

= \yz.z, by beta_I