Substitution is objective (I)

Context:

- While writing I searched for linear lambda calculus with copy and found

  Operational aspects of linear lambda calculus, P. Lincoln, J. Mitchell, (1992) Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science  

 I adapted then the naming to be compatible (naively) with that reference, but without the weight of linear logic. Maybe it is the same thing, maybe not, anyway all misinterpretations are due to my ignorance. 

- I use the asemantic computing draft

Continues with: Substitution is objective (II)

Main:

Decentralized reduction of lambda terms is problematic because of substitution. Indeed, where to make the substitution of a variable with a term, without any global information? Substitution of variables by terms is objective, that is it is not up to any discussion, but the problem appears when there is more than one place where substitution is made. [Added: the "real", "objective" language terms were explained many times, but on telegra.ph only here.]

With global information available, we know how to do reduction by using de Bruijn notation. We might use the calculus proposed in

 A λ-calculus à la de Bruijn with explicit substitutions, F. Kamareddine, A. Rios, 7th international conference on Programming Languages: Implementation, Logics and Programs, PLILP95, LNCS 982, 45-62

which makes very clear that beta reduction is mainly an icing of a big cake made of alpha renaming.

Such a notation (and such a calculus) is objective and global. It is not asemantic.

Substitution of variables by terms is local for linear lambda terms. It can be made local even for lambda terms which are not linear, by looking at the SKI calculus. 

Let's explore how we can make this work.

The S combinator in lambda calculus

 S = \a.\b.\c.((a c) (b c))

contains the c variable 3 times.

S is not "linear", where "linear" just means (classically) that any free variable appears once, any bounded variable appears twice (counting also the first appearance in a lambda operation. But we could make it like this if we introduce a "copy", which has the lambda-like notation:

 =x.T  where: x is a variable and T is a term

This reads "copy T to x" and it should mean something like this:

{  x = T;     \\ or "store T in x" ?

   return T; }

Then S will look like this:

 S = \a.\b.\c.((a d) (b (=d.c)))

or maybe like this?

 S = \a.\b.\c.((a (=d.c)) (b d))

or perhaps we should just use the copy at the beginning

 S = \a.\b.\(=d.c).((a c) (b d))

Now we see that S contains an abstracted fanout:

 \(=d.c).T

where c, d are variables and T is a (linear perhaps) lambda term.

We can transform any lambda term into an SKI combinator and back into a new lambda term, where every variable appears at most 3 times. It follows that we might just use SKI reduction rules translated into lambda calculus with the abstracted fanouts notation.

But how? For example

 S A B C -> (A C) (B C)

would become after 3 beta reductions

 (((\a.\b.\(=d.c).((a c) (b d))) A) B) C

 -> \(=d.C).((A C)(B d))

where the 3rd beta reduction is

 (\(=d.c).((A c)(B d))) C

 -> \(=d.C).((A C)(B d))

 Now we apply a kind of beta reduction (or is it a duplication?) adapted for the copy operation

  "copy-beta":   \(=d.C).T -> T[d=C]

which gives

  -> \(=d.C).((A C)(B d))

  -> (A C) (B C)

 provided that C is linear.

Also

 S K K -> I

would become

 ((\a.\b.\(=d.c).((a c) (b d))) (\x.\y.x)) (\z.\u.z)

 -> \(=d.c).(((\x.\y.x) c)((\z.\u.z) d))

 -> \(=d.c).((\y.c) (\z.d))

 -> \(=d.c).c

and the last step would be a sort of

 "discard":  if d does not occur free in T then \(=d.c).T -> \c.T

which gives in our case

 -> \(=d.c).c

 -> \c.c

Let's see the omega combinator (in the SKI translation)

 (S I I) (S I I)

 First remark that (S I I) would become

  ((\a.\b.\(=d.c).((a c) (b d))) (\x.x)) (\z.z)

  -> \(=d.c).(c d)

 therefore the omega combinator would look like

  (\(=d.c).(c d)) (\(=e.f).(f e))

  -> (\(=d.(\(=e.f).(f e))).((\(=e.f).(f e)) d))

 ... oups, not linear? Nah, it is all right, we just have to finish with a copy-beta reduction:

 -> (\(=d.(\(=e.f).(f e))).((\(=e.f).(f e)) d))

  -> (\(=e.f).(f e)) (\(=e.f).(f e))

which is linear.

 Conclusion: We proposed the following algorithm:

 1- Input a lambda calculus combinator A

 2- Convert A into SKI, obtain the combinator B

 3- Replace in B each instance of S, K, I with their lambda (plus copy) expressions

 4- Reduce using beta, copy-beta and discard.

Alternatively we may start with a linear (plus copy) term and jump directly to step 4.

We get a hint why chemSKI works in an asemantical way: because S encapsulates an objective substitution, thus making it local.