[ Jocelyn Ireson-Paine's Home Page | Publications | Interactive Category Theory Demonstrations | n-Category Café thread about Graphical Category Theory Demonstrations ]

System Limit Programming

This demonstrates a compiler I experimented with for mechanising Goguen's sheaf semantics of interacting objects, as described in Sheaf Semantics for Concurrent Interacting Objects.

The input to the SLP compiler describes types of components (such as amplifier and inverter), names instances of these components, and specifies how these instances are interconnected. The compiler works in three stages. In the first stage, it reads its input and generates from it the corresponding system diagram. In the second stage, it calculates a symbolic expression for the limit of this diagram in terms of products and equalisers. In the third stage, it evaluates this expression over the category of descriptions, generating a description of the limiting behaviour. This can then be run. It's only the third stage which depends on the structure of the descriptions: here, the compiler has to know how to form products of descriptions, and how to form equalisers from description morphisms.

First stage

One could force the user to input the system diagram directly. However, that requires him to think in an unfamiliar way: in particular, he would have to put in the "language objects" (which you denote by a curly E) to form the valley diagrams for interconnected components. So the compiler does that itself. The code below is a sample of the input: when the compiler sees "a1 joins_to a2", it knows it must construct a valley diagram:

amplifier(N) has_description    % Amplifies X N times to make Y.
  ( s([X,Y]) :- Y is N*X ).

a1 is_a amplifier(11).          % Amplifies by 11.

a2 is_a amplifier(22).          % Amplifies by 22.

a1 joins_to a2.                 % a2 amplifies a1's output.

Second stage

This uses a recursive algorithm to calculate an expression for the limit of the system diagram in terms of products and equalisers. I based the algorithm on an account in Computational Category Theory by Rydeheard and Burstall. The compiler assumes the category of descriptions has limits, but doesn't check this. In essence, the result of the limit calculation is just a term over the following signature, and consists of a chain of equalisers terminated by a product:

sort Object Arrow .
op   compose   : Arrow Arrow -> Arrow .
op   product   : Object Object -> Object .
op   equaliser : Arrow Arrow -> Object .

The product gives the behaviour the system would have if there were no interactions between components, and the equalisers add the constraints imposed by these interactions.

Third stage

Here, the compiler just reduces the limit term by forming products and equalisers of the descriptions in the input. It's during this stage (only) that it needs a description-specific set of functions to do this, so this is the only time it worries about the structure of the category of descriptions.

Worked example

Now I'll describe briefly the descriptions I used in the circuit example. A circuit consists of input-output elements and wires. I don't consider time (base = one-point set), so the behaviour of any component collapses to a set of tuples. These can be described by Prolog clauses which will accept (or generate) only those tuples. So:

s(_)            A language object: all voltages.
s(5)            The constant input 5.
s([X,Y]) :-
  Y is 10*X.    A 10-times amplifier. Behaviour is described
                by pairs, where the output Y = 10 times the
                input X.

Then the product of two descriptions:

s(A1,...Am) :- p(A1,...Am).
s(B1,...Bn) :- q(B1,...Bn).
is the clause which accepts any combination of the tuples represented by the argument lists:
s(A1,...Am, B1,...Bn) :- p(A1,...Am), q(B1,...Bn).

Equalisers are more complicated because they depend on the structure of the arrows. For example, suppose we have two arrows a1 and a2 from a product P to a wire language-object W. And suppose that a1 is just a projection pi1. a2 is the composition pi2 ; i where pi2 is a projection from P to a constant input C, and i is an inclusion from C to W. This situation arises when connecting a circuit element to a constant input.

Then to make the equaliser of a1 and a2, we take the clause corresponding to P, and we add a new conjunct in its tail which unifies the arguments in its head corresponding to projections pi1 and pi2.

Demonstration 1

First, I load my SLP demo. This loads the SLP compiler into Poplog Prolog:

?- reconsult('slp.pl').
;;; DECLARING VARIABLE get_prompt
;;; DECLARING VARIABLE set_prompt
yes

It also loads this SLP program, describing a circuit:

inverter has_description
    ( s([X,Y]) :- Y is -X ).

wire has_description
    s(_).

i is_a inverter.

p1 is_a wire.
p1 has_description
    s(5).

p1 joins_to i.

p2 is_a wire.
p2 has_description
    (s(Result) :- write('Output = '), write(Result), nl).

i joins_to p2.

Next, I ask the compiler to display the diagram it has made from this program:

?- testc.
slp_object(individual, active_element, inverter, i).
slp_object(individual, wire, p1, p1).
slp_object(individual, wire, p2, p2).
slp_object(input, wire(p1, i), wire, wire0).
slp_object(output, wire(i, p2), wire, wire1).

slp_arrow(inclusion, p1, wire0).
slp_arrow(port(1), i, wire0).
slp_arrow(port(2), i, wire1).
slp_arrow(inclusion, p2, wire1).

It also shows me the limit object it has calculated, and a Prolog clause corresponding to this object, and the result of running the clause:

Limit object = 
eq(eq(eq(eq(i*p1*p2*wire0*wire1->wire1)->wire0)->wire1)->wire0
	)

s([_1, _2], 5, _3, _4, _5) :- ((((_2 is - _1, write(Output = ), write(_3),
	 nl), _5 = _2), _4 = _1), _5 = _3), _4 = 5

Output = -5
yes

Demonstration 2

This calculates the result of a more complicated program:

amplifier(N) has_description
    ( s([X,Y]) :- Y is N*X ).

wire has_description
    s(_).

a1 is_a amplifier(11).

a2 is_a amplifier(22).

p1 is_a wire.
p1 has_description
    s(5).

p1 joins_to a1.

a1 joins_to a2.

Here is the diagram the compiler derives from it:

?- testc2.
slp_object(individual, active_element, amplifier(11), a1).
slp_object(individual, active_element, amplifier(22), a2).
slp_object(individual, wire, p1, p1).
slp_object(individual, wire, p2, p2).
slp_object(input, wire(p1, a1), wire, wire2).
slp_object(connection, wire(a1, a2), wire, wire3).
slp_object(output, wire(a2, p2), wire, wire4).

slp_arrow(inclusion, p1, wire2).
slp_arrow(port(1), a1, wire2).
slp_arrow(port(2), a1, wire3).
slp_arrow(port(1), a2, wire3).
slp_arrow(port(2), a2, wire4).
slp_arrow(inclusion, p2, wire4).

And here are the limit object, the corresponding Prolog clause, and its output:

Limit object = 
eq(eq(eq(eq(eq(eq(a1*a2*p1*p2*wire2*wire3*wire4->wire4)->wire3
	)->wire3)->wire2)->wire4)->wire2)

s([_1, _2], [_3, _4], 5, _5, _6, _7, _8) :- ((((((_2 is 11 * _1, _4 is
	 22 * _3, write(Output = ), write(_5), nl), _8 = _4), _7 = _2),
	 _7 = _3), _6 = _1), _8 = _5), _6 = 5

Output = 1210
yes

Demonstration 3

This time, we calculate the colimit of theories describing the components of a circuit, rather than the limit of their behaviours. Here is the input:

inverter has_description
    th( [voltage],                            /* Shared sort        */
        [inverter],                           /* sort inverter .    */
        [[i,[],inverter],                     /* op i -> inverter . */
         [input,[inverter],voltage],          /* op input : inverter -> 
voltage .  */
         [output,[inverter],voltage]          /* op output : inverter 
-> voltage . */
        ],
        [ apply(output,[i]) = apply(-,[apply(input,[i])]) ]
                                              /* eq output i = - input i . 
*/
      ).

wire has_description
    th( [voltage],                            /* Shared sort        */
        [wire],                               /* sort wire .        */
        [[w,[],wire],                         /* op w -> wire .     */
         [value,[wire],voltage]               /* op value : wire -> 
voltage .      */
        ],
        [ ]
      ).

i is_a inverter.

p1 is_a wire.
p1 has_description
    th( [voltage],                            /* Shared sort        */
        [wire],                               /* sort wire .        */
        [[w,[],wire],                         /* op w -> wire .     */
         [value,[wire],voltage]               /* op value : wire -> 
voltage . */
        ],
        [ apply(value,[w]) = 5 ]              /* eq value w = 5 .   */
      ).

p1 joins_to i.

p2 is_a wire.
p2 has_description
    th( [voltage],
        [wire],
        [[w,[],wire],
         [value,[wire],voltage]
        ],
        [ apply(value,[w]) = ? ]
      ).

i joins_to p2.

This is the resulting diagram:

?- testcth.
slp_object(individual, active_element, inverter, i).
slp_object(individual, wire, p1, p1).
slp_object(individual, wire, p2, p2).
slp_object(input, wire(p1, i), wire, wire8).
slp_object(output, wire(i, p2), wire, wire9).

slp_arrow(inclusion, p1, wire8).
slp_arrow(port(1), i, wire8).
slp_arrow(port(2), i, wire9).
slp_arrow(inclusion, p2, wire9).

And here are its colimit object, the resulting colimit theory in internal representation, and it pretty-printed:

Limit object = 
eq(eq(eq(eq(i*p1*p2*wire8*wire9->wire9)->wire8)->wire9)->wire8
	)

th(i * (p1 * (p2 * (wire8 * wire9))), [voltage], [dot(i, inverter), 
dot(p1,
	 wire), dot(p2, wire), dot(wire8, wire), dot(wire9, wire)], 
[[dot(i,
	 i), [], dot(i, inverter)], [dot(i, input), [dot(i, inverter)],
	 voltage], [dot(i, output), [dot(i, inverter)], voltage], [dot(p1,
	 w), [], dot(p1, wire)], [dot(p1, value), [dot(p1, wire)], 
voltage],
	 [dot(p2, w), [], dot(p2, wire)], [dot(p2, value), [dot(p2, 
wire)],
	 voltage], [dot(wire8, w), [], dot(wire8, wire)], [dot(wire8,
	 value), [dot(wire8, wire)], voltage], [dot(wire9, w), [], 
dot(wire9,
	 wire)], [dot(wire9, value), [dot(wire9, wire)], voltage]], 
[apply(do
	t(p1, value), [dot(p1, w)]) = apply(dot(wire8, value), [dot(wire8,
	 w)]), apply(dot(p2, value), [dot(p2, w)]) = apply(dot(wire9,
	 value), [dot(wire9, w)]), apply(dot(i, input), [dot(i, i)]) =
	 apply(dot(wire8, value), [dot(wire8, w)]), apply(dot(wire9, 
value),
	 [dot(wire9, w)]) = apply(dot(i, output), [dot(i, i)]), 
apply(dot(i,
	 output), [dot(i, i)]) = apply(dot(i, -), [apply(dot(i, input),
	 [dot(i, i)])]), apply(dot(p1, value), [dot(p1, w)]) = 5, 
apply(dot(p
	2, value), [dot(p2, w)]) = dot(p2, ?)])

THEORY i * (p1 * (p2 * (wire8 * wire9)))
  includes sorts voltage
  sorts i.inverter p1.wire p2.wire wire8.wire wire9.wire
  ops i.i:->i.inverter
      i.input:i.inverter->voltage
      i.output:i.inverter->voltage
      p1.w:->p1.wire
      p1.value:p1.wire->voltage
      p2.w:->p2.wire
      p2.value:p2.wire->voltage
      wire8.w:->wire8.wire
      wire8.value:wire8.wire->voltage
      wire9.w:->wire9.wire
      wire9.value:wire9.wire->voltage
  eq p1.value(p1.w) = wire8.value(wire8.w)
  eq p2.value(p2.w) = wire9.value(wire9.w)
  eq i.input(i.i) = wire8.value(wire8.w)
  eq wire9.value(wire9.w) = i.output(i.i)
  eq i.output(i.i) = i.-(i.input(i.i))
  eq p1.value(p1.w) = 5
  eq p2.value(p2.w) = p2.?

yes

Jocelyn Ireson-Paine
14 November 2014