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.
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.
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 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.
Here, the compiler 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.
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 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.
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
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
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