Lambda Calculus With Variables, Without Substitution

[Rock Brentwood]

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

[William Elliot]

Post by Rock Brentwood
You read it right: "... WITHOUT Substitution."

Read what right?

Post by Rock Brentwood
So, what's the trick?

Trick to what?

Post by Rock Brentwood
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.

Use of catogory theory complicates any discussion.
Ok, you reveiw the rules of the Calculi of Lambda
and go into some calulations about S and K, two spacific lambda
formulas. Interesting think about S and K is that every lambda
calulus forumla can be show to be extensionally equal or equivalent
to a combination of S's and K's. There are other more intuitive
sets of fumulas that can be used for the combinatorial calculi,
but { S,K } is the smallest.

Post by Rock Brentwood
\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.
@(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.
* 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)).
beta: (\x.T)U = (x = U, T)
sigma_I: (x = U, x) = U
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
(x = U, \y.T)
= (x = U, \z.(y = z.T))
= \z.(x = U, (y = z, T))
U, T).
So ... after treating beta as a definition, applying it to the alpha
and sigma rules to eliminate all the substitutions and then
* beta_I: (\x.x)T = T
* beta_S: (\x.TT')U = (\x.T)U ((\x.T')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
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.
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

[Rock Brentwood]

Post by William Elliot

Post by Rock Brentwood
You read it right: "... WITHOUT Substitution."

Read what right?

Post by Rock Brentwood
So, what's the trick?

Trick to what?

It's illogical to ask a question in direct reply to its own answer
(i.e. the subject header of the original article); and disingenuous to
delete the answer in reply to your own question (by changing the
subject header from what it originally was).

[William Elliot]

Post by Rock Brentwood

Post by William Elliot

Post by Rock Brentwood
You read it right: "... WITHOUT Substitution."

Read what right?

Post by Rock Brentwood
So, what's the trick?

Trick to what?

It's illogical to ask a question in direct reply to its own answer
(i.e. the subject header of the original article); and disingenuous to
delete the answer in reply to your own question (by changing the
subject header from what it originally was).

Titles are not part of the message.
Titles simply indicate the topic.
Additionally, in this media, titles can and do change.

We could have been discussing math, but no, it was more
important for you to defend your ignorant misuse of titles.

Do you want to talk about combinatorial calculi or not?