__Canonical string reduction__

This note addresses the problem of how to characterize an intermediate machine state during the evaluation of a SASL expression. Addressing that problem without any specific implementation in mind and observing that both the initial state and the answer are legitimate SASL expressions, I shall try to characterize the relevant intermediate states as SASL expressions as well. In doing so I hope to design such a strict scheme for using scopes that some light is shed on the problem of garbage detection.

I have to adapt SASL's syntax to my purpose. Instead of writing

from 0I shall writewherefrom n = n : from (n+1)

|[ fromThe inner block on the middle line delineates the scope of n ; the fact that it ends on "withfrom = |[ n : from (n+1)withn= ]| ]| 0

know better as the λ-expression λn • (n:from(n+1)). The outer block delineates the scope of the identifier from . Its first occurrence states that the whole block stands for the object locally known as "from"; "__with__ from = " introduces a definition of the object locally known as "from"; the object being a function, its definition then follows as a λ-expression. Note the contrast with the original SASL program: there the whole expression "from 0" was defined with the scope of "from", while in our version the scope of "from" is chosen as small as possible.

We shall do our experiments with a slightly more ambitious program, viz. the program for the tabulation of fusc, inspired by J.L.A. van de Snepscheut, designed by A.J.M. van Gasteren, and using the function "zip" as simplified by F.E.J. Kruseman Aretz.

In regular SASL the text could be

xThe above definition fails to express very directly - i.e. otherwise than by the recognition of the pattern "b:c" - that the tail of the original argument of elf is the argument of the recursive call.wherex = 1 : zip x (elf x)wherezip (p:q)r = p : zip r q elf(a:b:c) = a+b:elf(b:c)

In our notation, we would write

|[ xThe scope of x extends over 0-11; the scope of zip extends over 1-5; the scope of p:q extends over 2-4; the scope of r is on line 3; the scope of elf extends over 6-10; the scope of a:y extends over 7-9; the scope of b is on line 8.withx = 1: (0) |[ zipwithzip= (1) |[ p: (2) |[ zip r qwithr= ]|withp:q= (3) |] (4) |] x (5) ( |[ elfwithelf= (6) |[ a + (7) |[ bwithb:?=y]| : elf ywitha:y= (8) ]| (9) ]| x) (10) ]| (11)

The definition of zip on 2-4 is arrived at by successive abstraction. From

zip (p:q) r = p:zip r qwe derive, by abstracting first from r,

zip (p:q) = p : |[ zip r qHere, the proper scope for r has been determined as follows: the placing of "withr= ]| .

corresponding "|[" is determined by the rule that the scope coincides with the smallest syntactic unit containing all occurrences of the variable in question. Here its place reflects that functional application is left-associative, i.e. that zip r q is short for ((zip r) q).

On line 8, |[ b __with__ b:?=y ]| is no more than a complicated way of writing "hd y". The convention followed seems consistent - it is, in terms of number of characters needed, clumsy, but that is of no relevance here: we are not proposing a notation to be programmed in.

Things defined within a scope are significant within that scope. Our final result should have global significance. This observation presents the process of evaluation as exporting successive elements of x - which is a continued concatenation of integers - outside the scope of the local terminology. (We had already decided to choose our scopes as small as possible; exporting as much as possible from them is a natural extension. It can be claimed that we already did so, when we replaced

|[ p : zip r qEvaluation of an expression can now be viewedwithr= ]| by p : |[ zip r qwithr= ]| . )

as applying such reductions (i.e. semantics preserving transformations) that lead to export from a scope of values global with respect to that scope.

In this case we can do that by substitution. We have an expression of the form

|[ xThe substitution x = 1:w - meaningful because "1" has a meaning outside the scope of x - leads to the equivalent, but further evaluated expressionwithx = 1: E(x) ]| .

1:|[ wThe inner bracket pair delineates the scope of x, the outer bracket pair delineates the scope of w.withw = |[ E(x)withx=1:w ]| ]| .

Applying the substitution x=1:w we get

1:|[ wThis is, to my feeling,withw = (0) |[ |[ zipwithzip = (1) |[ p: |[ zip r qwithr = ]|withp:q= ]| (2) ]| x (3) (|[ elfwithelf= (4) |[a + |[ bwithb:?=y ]| : elf ywitha:y= ]| (5) ]| x)withx = 1:w (6) ]| (7) ]| (8)

- by substituting 1:w for it - since, within its scope, x is referenced twice. The next thing to do is to unfold zip, i.e. replacing its outer occurrence by its definition and inserting its definition at its inner occurrence, i.e. replacing lines (1), (2), and (3) by

|[ |[ p: |[ |[ zipApplication of the above unfolded zip to x=1:w leads to the elimination of the outer p:q, i.e. the above can be simplified towithzip = |[ p: |[ zip r qwithr = ]|withp:q = ]| ]| r qwithr = ]|withp:q = ]|

|[ 1: |[ |[ zipWe can now eliminate x by replacing its last occurrence by (1:w). The above being applied to the expression of 4-6, we also eliminate in the above the outer r, which is only referenced once. The combined result of these eliminations iswithzip = |[ p : |[ zip r qwithr = ]|withp:q = ]| ]| r wwithr = ]|

1: |[ wThe next step is one we have seen before, viz substitution. This time we substitute something for w, say 1:x. The result iswithw = 1: |[ zipwithzip = |[ p: |[ zip r qwithr = ]|withp:q= ]| ]| (|[ elfwithelf= |[ a+ |[ bwithb:?=y ]| : elf ywitha:y= ]| ]| (1:w)) w ]|

1:1: |[ xAgain, I have not felt the liberty of eliminating w, being referenced twice. The next step is to unfold zip again. In order to save writing I have performed the subsequent unfolding of elf as well.withx = |[ |[ zipwithzip= |[ p : |[ zip r qwithr = ]|withp:q= ]| ]| (|[ elfwithelf= |[ a+ |[ bwithb:?=y]| : elf ywitha:y= ]| ]| (1:w)) wwithw=1:x ]| ]|

1:1: (0) |[ xNow we are ready to eliminate the outer a:y scope. Lines 8-12 become thenwithx= (1) |[ |[ p: (2) |[ |[ zipwithzip= (3) |[ p: |[ zip r qwithr= ]|withp:q= ]| (4) ]| r qwithr= (5) ]|withp:q= (6) ]| (7) (|[ a+ |[ bwithb:?=y]|: (8) |[ elfwithelf= (9) |[ a+ |[ bwithb:?=y]| : elf ywitha:y= ]| (10) ]| ywitha:y= (11) ]| (1:w)) wwithw=1:x (12) ]| (13) ]| (14)

(1 + |[ bNow we can do several things. On account of w=1:x the top line of the above can be replaced by "(1+1:" and then by "(2:". We can also eliminate the outer p:q scope. They commute; then the outer r scope can be eliminated.withb:?=w ]|: |[ elfwithelf= |[ a + |[ bwithb:?=y ]| : elf ywitha:y= ]| ]| w ) wwithw = 1:x

1:1: |[ xBut now I get into problems. Taking the definitions of zip and elf for granted, the above can be represented aswithx=2: |[ |[ zipwithzip = |[ p: |[ zip r qwithr = ]|withp:q= ]| ]| w (|[ elfwithelf= |[ a+ |[ bwithb:?=y ]| : elf ywitha:y = ]| ]| w)withw=1:x ]| ]|

1:1: |[ xand in a really demand-driven mode we would substitute x=2:y and we would getwithx = 2: |[ zip w (elf w)withw = 1:x ]| ]|

1:1:2: |[ yOne way to proceed would be to eliminate the scope of x:withy= |[ |[ zip w (elf w)withw = 1:x ]|withx = 2:y ]| ]|

1:1:2: |[ ywithy = |[ zip w (elf w)withw = 1:2:y ]| ]|

followed by an application of zip

1:1:2: |[ yfollowed by removal of w's single reference:withy = 1 : |[ zip (elf w) (2:y)withw = 1:2:y ]| ]|

1:1:2: |[ yOn the other hand, in a truly demand-driven way, we could have applied zip, using w=1:xwithy = 1: zip (elf(1:2:y)) (2:y) ]|

1:1:2: |[ yfollowed by a removal of w's single referencewithy = 1: |[ |[ zip (elf w) xwithw=1:x ]|withx = 2:y ]| ]|

1:1:2: |[ yI like that last form better, and consider the early removal of the scope of x - on account of "single occurrence" - a mistake. Let us, therefore, try only to substitute when forced to do so by a function application. Let us redo the game, but now in shorthand.withy=1: |[ zip (elf(1:x)) xwithx=2:y ]| ]|

|[ xThe introduction x = 1:w leads towithx = 1 : zip x (elf x) ]|

1 : |[ wApplication of zip forces the first x to be substitutedwithw = |[ zip x (elf x)withx = 1:w ]| ]|

1 : |[ wThe introduction of w = 1:y leads towithw = 1 : |[ zip (elf x) wwithx = 1:w ]| ]|

1:1:|[ yApplication of elf is now possible, and the scope for x disappearswithy = |[ |[ zip (elf x) wwithx = 1:w ]|with1 = 1:y ]| ]|

1:1: |[ yNow zip can be appliedwithy = |[ zip (2:(elf w)) wwithw = 1:y ]| ]|

1:1: |[ ySubstituting y = 2:x we getwithy = 2: |[ zip w (elf w)withw = 1:y ]| ]|

1:1:2: |[ xNext we apply zip, using w = 1:y oncewithx = |[ |[ zip w (elf w)withw = 1:y]|withy = 2:x ]| ]|

1:1:2: |[ xEtc. In this way the dilemma does not emerge. We need, of course, more and more identifiers, but that does not matter. We could use f[k:k≽0]; f[k] stands then for (+e)withx = 1 : |[ |[ zip (elf w) ywithw=1:y ]|withy= 2:x ]| ]|

It is very well possible that the above example is much too simple. It suggests me, that garbage detection should not be a serious problem, and that should make me suspicious.

__Note__. I have not __proved__ that with my last regime the dilemma does not arise, for the time being I am willing to believe it. (I am very willing to believe that the dilemma does not arise this way, for it is exactly the place where I got stuck a year ago). (End of Note.)

Plataanstraat 5 5671 AL NEUNEN The Netherlands |
16 December 1981 prof.dr.Edsger W. Dijkstra Burroughs Research Fellow |

Transcribed by Mikhail Esteves

Last revised on