Lambda Expressions


Introduction

Motivation describes the motivation for our project. There, we recognise that there are many different views of systems structure, expressed in many different languages, and that these different views need to be related together. However, our experiences, over fifty years, tells us that the languages get in the way of this "relating together". They make rigid distinctions between things that are not fundamentally different, e.g. programs and data, procedures and interfaces, types and instances, processes and transactions, etc. Worse still, the strong distinctions made by each language are inconsistent with the distinctions made by other languages. We therefore want to get away from these distinctions and start from an extremely simple semantics.

We have developed a very simple modelling style that matches our motivation and enables us to relate together the many interacting views of system structure that were referred to above. The primitive semantics of this modelling style has just one type of object - a system, and one type of relationship connecting such objects - a role of a system as a component in another system. We show that this modelling style can cope with the full range of mathematical and business problems, and can be related to other modelling styles.

A wide range of computational problems can be solved using lambda expressions, so it seems sensible for us to see how they can be expressed in our programming style; hence this document. In tackling lambda expressions, we make use of syntactic sugar introduced in Programming Manual, in particular the contextual bind operation =c.


Lambda Expression ( (λ a (λ t (a) ) ) f) t

How would lambda expressions be held and evolved in our graphs C and S? Consider the lambda expression ( (λ a (λ t (a) ) ) f) t. We believe that this lambda expression and its reductions would appear in the graphs C and S as:-

where α is used for application, λ for abstraction, p for parameter, and e for expression. In the diagram, a=f means that the system, which had the label 'a' at the human interface, is turned into a copy of the system that had the label 'f', i.e. it is given the component structure of that system; in this case (a=f) the new and old component structures are similar but that will not always be the case.

Each application of an abstraction requires the following graph transformations on C - expressed relative, within the toatal lambda expression, to the abstraction being applied, as illustrated in the diagram:-

Here parent means the application expression that is applying this abstraction expression (the one that has the abstraction as its component with role identified by 'e'), grandparent means whatever is invoking the parent application expression (whatever has the application as its component expression with role identified by 'e').

The code for an abstraction expression needs two routes through it; the first route is taken when it is invoked from somewhere other than an application expression and does very little (just activates the route 1 code of its component expression with role identified by 'e'); the second route is taken when it is invoked from the code of an application expression and it then performs the three graph transformations outlined above.

The code for an application expression also need two routes through it, with both routes doing very little (just activating the route 2 code of its component expression with role identified by 'e').

If the code for constant expression (e.g. t, a and f in the above) is entered, it means that the evaluation of the total lambda expression has got as far as it can and so we need to exit the total evaluation. Hence, the code for a constant expression also need two routes through it, with both routes doing very little (just invoking the continuation program of the total lambda expression).

Thus, the lambda expression ( (λ a (λ t (a) ) ) f) t needs to be turned into the following program in our modelling style:-

       ≺e≻
       ≺
          ≺complex-type≻≺applicationc≻, ≺parent≻≺HOLE≻,
          ≺route1≻≺applicationcode≻,
          ≺route2≻≺applicationcode≻,
          ≺p≻≺t1 ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻, ≺route2≻≺constantcode≻ ≻,
          ≺e≻
          ≺
             ≺complex-type≻≺applicationc≻, ≺parent≻≺HOLE≻,
             ≺route1≻≺applicationcode≻,
             ≺route2≻≺applicationcode≻,
             ≺p≻≺f ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻, ≺route2≻≺constantcode≻ ≻,
             ≺e≻
             ≺
                ≺complex-type≻≺abstractionc≻, ≺parent≻≺HOLE≻,
                ≺route1≻≺inactiveabstractioncode≻,
                ≺route2≻≺activeabstractioncode≻,
                ≺p≻≺a ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻ ≺route2≻≺constantcode≻ ≻,
                ≺e≻
                ≺
                   ≺complex-type≻≺abstractionc≻, ≺parent≻≺HOLE≻,
                   ≺route1≻≺inactiveabstractioncode≻,
                   ≺route2≻≺activeabstractioncode≻,
                   ≺p≻≺t2 ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻ ≺route2≻≺constantcode≻ ≻,
                   ≺e≻≺a≻
       ≻≻≻≻

The above program could be input, to graph C, at the human interface, as a reification of the lambda expression ( (λ a (λ t (a) ) ) f) t. Once it is in C, all of the labels (e.g. t, f, a, type, applicationcode, constantcode, route1, continue, etc.) will have disappeared and been replaced by nodes (systems) in graph C. Where the same label appeared in multiple places within the text, they will all have been replaced with just one, shared, node (system) in graph C (note that in the text above we had to replace the two occurences of 't' in ( (λ a (λ t (a) ) ) f) t with t1 and t2; this was because the nested structure of the lambda expression ( (λ a (λ t (a) ) ) f) t implies they are different).

Of course, the interpretation of the above program would occur entirely within graph C and so the labels would not reappear during the interpretation. However, we can imagine that the program is displayed, at the human interface, at the end of each stage in its interpretation, and so can show the labels, below.

Because of the definitions, concerning routes, given before the above code, we know that the 'activeabstractioncode' in the third level of the expression is able to take effect, so that the total lambda expression is transformed into:-

       ≺e≻
       ≺
          ≺complex-type≻≺applicationc≻, ≺parent≻≺HOLE≻,
          ≺route1≻≺applicationcode≻,
          ≺route2≻≺applicationcode≻,
          ≺p≻≺t1 ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻, ≺route2≻≺constantcode≻ ≻,
          ≺e≻
          ≺
             ≺complex-type≻≺abstractionc≻, ≺parent≻≺HOLE≻,
             ≺route1≻≺inactiveabstractioncode≻,
             ≺route2≻≺activeabstractioncode≻,
             ≺p≻≺t2 ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻ ≺route2≻≺constantcode≻ ≻,
             ≺e≻≺a=f ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻ ≺route2≻≺constantcode≻ ≻
       ≻≻

Now, the 'activeabstractioncode' in the second level of the expression is able to do its work, and the total expression is transformed into:-

       ≺e≻
       ≺a=f ≺complex-type≻≺constantc≻, ≺route1≻≺constantcode≻ ≺route2≻≺constantcode≻ ≻

with this becoming the component system, with role identified by 'e', in the program that originally invoked the expansion of the lambda expression.

Note, that, in the above, the total code for each abstraction, application and constant is not reusable; there needs to be a fresh copy for each abstraction, application and constant. It is the pieces of code for the various routes through them that are reusable.

Now, we need to provide the four pieces of code 'applicationcode', 'constantcode', 'inactiveabstractioncode' and 'activeabstractioncode'. The fourth of these pieces of code needs access to the components of the two levels of expression (parent and grandparent) above the one containing it - this is achieved by each level of expression having a 'parent' component. All four pieces of code need access to the components of the level of expression containing it - this is achieved by the level of expression that is currently being interpreted having an 'expression' role within the interpreter.

The 'applicationcode' then needs to be:-

       ≺applicationcode
          ≺type≻≺=c≻, ≺2≻≺expression.¿≻, ≺4≻≺expression.e.parent≻, ≺cont≻≺current.continue≻,
          ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺expression.e≻, ≺4≻≺expression.¿≻, ≺cont≻≺expression.route2≻ ≻
       ≻

The second line makes the current level of the expression the parent for the next level down. The third line activates the next level down of the expression and enters the code for its second route.

The 'inactiveabstractioncode' needs to be almost identical, except that it exits to the first level code in the next level:-

       ≺inactiveabbstractioncode
          ≺type≻≺=c≻, ≺2≻≺expression.¿≻, ≺4≻≺expression.e.parent≻, ≺cont≻≺current.continue≻,
          ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺expression.e≻, ≺4≻≺expression.¿≻, ≺cont≻≺expression.route1≻ ≻
       ≻

The 'constantcode' just needs to exit to the continuation program for the whole lambda expression:-

       ≺constantcode ≺type≻≺=c≻, ≺cont≻≺continuation.¿≻ ≻

The 'activeabstractioncode' is more complicated, because it needs to perform the three graph transformations:-

This needs the following:-

       ≺activeabstractioncode
          ≺complex-type≻≺copycomponentsc≻, ≺source≻≺expression.parent.p≻, ≺destination≻≺expression.p≻, ≺contn≻≺current.continue1≻,
          ≺continue1≻≺ ≺type≻≺=c≻, ≺2≻≺expression.e≻, ≺4≻≺expression.parent.parent.e≻, ≺cont≻≺current.continue≻,
                                     ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺expression.parent.parent≻, ≺4≻≺expression.¿≻, ≺cont≻≺expression.route1≻ ≻
       ≻ ≻

where the second third and fourth lines perform the three graph transformations outlined above and the complex type 'copycomponentsc' has the expansion:-

       ≺
          ≺complex-type≻≺copycomponentsc≻, ≺source≻≺src≻, ≺destination≻≺dest≻, ≺contn≻≺continuation≻,
          ≺type≻≺=c≻, ≺2≻≺src.p≻, ≺4≻≺dest.p≻, ≺cont≻≺current.continue≻,
          ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺src.e≻, ≺4≻≺dest.e≻, ≺cont≻≺current.continue≻,
                                   ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺src.route1≻, ≺4≻≺dest.route1≻, ≺cont≻≺current.continue≻,
                                                            ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺src.route2≻, ≺4≻≺dest.route2≻, ≺cont≻≺current.continue≻,
                                                                                     ≺continue≻≺ ≺type≻≺=c≻, ≺2≻≺src.complex-type≻, ≺4≻≺dest.complex-type≻, ≺cont≻≺continuation≻ ≻
       ≻ ≻ ≻ ≻

How about the program that activated the evaluation of the total lambda expression. This program needs to:-

This requires at least the following code:-

       ≺
          ≺type≻≺=c≻, ≺2≻≺current.¿≻, ≺4≻≺expression.¿≻, ≺cont≻≺current.continue≻, ≺continue≻≺inactiveabstractioncode≻,
          ≺route1≻≺ ≺type≻≺=c≻, ≺cont≻≺continuation.¿≻ ≻,
          ≺route2≻≺ ≺type≻≺=c≻, ≺cont≻≺continuation.¿≻ ≻,
          ≺e≻≺rest-of-expression≻
       ≻

invoked via its second line initially - the fourth line is invoked when the program is called as grandfather.

Given the above, we can translate any lambda expression into our modelling style.

In the Church representation of Booleans (followed by Milner in his work on pi-calculus) true is represented by the lambda expression λ a (λ b (a) ) and false by λ a (λ b (b) ). ∧ is then represented by λ a (λ b ( (a (b) ) a) ), and ∨ by λ a (λ b ( (a (a) ) b) ). In our programming style, a Boolean variable then has two components with roles identified by 'on' and 'off'. If the variable is in its true state then the component with role identified by 'on' is the true system (i.e. the sequence of binds for λ a (λ b (a) )), and the component with role identified by 'off' is the false system. If the Boolean variable is in its false state these components are reversed.