Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.functional > #176

Re: Lambda Calculus

Cross-posted to 2 groups.

Show all headers | View raw

On Fri, 30 Sep 2011, Rock Brentwood wrote:

> You read it right: "... WITHOUT Substitution."
>
Read what right?

> So, what's the trick?

Trick to what?

> 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.

> 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
>

Back to comp.lang.functional | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Lambda Calculus With Variables, Without Substitution Rock Brentwood <federation2005@netzero.com> - 2011-09-30 21:10 -0700
  Re: Lambda Calculus William Elliot <marsh@rdrop.com> - 2011-09-30 22:07 -0700
    Re: Lambda Calculus Rock Brentwood <federation2005@netzero.com> - 2011-09-30 22:14 -0700
      Composition, Coherence and Cognitive Thought William Elliot <marsh@rdrop.com> - 2011-09-30 23:31 -0700

csiph-web