Functions
Syntax
Define the language
RecFun(V,C,P)
as extending RecExp(V,C,P) with
new types:
T | ::= | ...as before... |
| | | C T : T |
and new expressions:
M | ::= | ...as before... |
| | | fn C P {M} | (Anonymous function) |
| | | M M | (Function application) |
The typing for anonymous functions is:
|
|
(P : T) : |
, |
|
M : T in C |
|
|
|
fn C P {M} : (C T : T) in val |
and for function application is:
|
|
M : (C T : T) in val |
|
|
M : T in C |
|
|
|
M M : T in C |
In particular, note that anonymous functions are always values,
even if the function body is central or process. This agrees with
the usual definition of normal forms for operational semantics.
Graphical semantics
Cartesian closed
To give a graphical semantics for the cartesian closed structure,
we extend the category of cyclic flow graphs
CGraph(V)
to that of closed cyclic flow graphs
CCGraph(V)
by allowing edges to be labelled by value function types:
A,B,C ::= X
| A1,...,Am
B1,...,Bn
and allowing nodes of the form:
with labellings:
:
(B1,...,Bn
C1,...,Co),
B1,...,Bn
C1,...,Co
in
CCGraph(V)
:
A1,...,Am
(B1,...,Bn
C1,...,Co)
in
CCGraph(V)
where:
:
A1,...,Am,
B1,...,Bn
C1,...,Co
in
CCGraph(V)
These graphs are factored up to the equivalence required for a cartesian
closed category:
CCGraph(V)[A, B C]
CCGraph(V)[A B, C]
Graphically these axioms are:
Beta: |
|
= |
|
Eta: |
|
= |
|
Naturality: |
|
= |
|
The graphical semantics is extended with:
[[fn val P {M} in val]] |
= |
|
[[M N in val]] |
= |
|
Symmetric monoidal closed
To give a semantics for the symmetric monoidal closed structure:
by allowing edges to be labelled by central function types:
A,B,C ::= ...
| A1,...,Am
B1,...,Bn
We extend flow graphs to allow nodes of the form:
with labellings:
:
(B1,...,Bn
C1,...,Co),
B1,...,Bn
C1,...,Co
in
CCGraph(V,C)
:
A1,...,Am
(B1,...,Bn
C1,...,Co)
in
CCGraph(V,C)
where:
:
A1,...,Am,
B1,...,Bn
C1,...,Co
in CCGraph(V,C)
These graphs are factored up to the equivalence required for
the adjunction:
CCGraph(V,C)[A, B C]
CCGraph(V,C)[A B, C]
Graphically:
Beta: |
|
= |
|
Eta: |
|
= |
|
Naturality: |
|
= |
|
The graphical semantics is extended with:
[[fn central P {M} in val]] |
= |
|
[[M N in central]] |
= |
|
Symmetric premonoidal closed
To give a semantics for the symmetric monoidal closed structure:
- we extend the category of cyclic flow graphs
CGraph(V,C,P)
to that of closed cyclic flow graphs
CCGraph(V,C,P),
- we extend the category
CCGraph(V,C)
to
CCGraph(V,C,P), and
- we extend the category
CCGraph(V,C)
to
CCGraph(V,C,P).
by allowing edges to be labelled with process function types:
A,B,C ::= ...
| A1,...,Am
B1,...,Bn
and allowing nodes of the form:
with labellings:
:
(B1,...,Bn
C1,...,Co),
B1,...,Bn
C1,...,Co
in
CCGraph(V,C,P)
:
A1,...,Am
(B1,...,Bn
C1,...,Co)
in
CCGraph(V,C,P)
where:
:
A1,...,Am,
B1,...,Bn
C1,...,Co
in
CCGraph(V,C,P)
These graphs are factored up to the equivalence required for
the adjunction:
CCGraph(V,C,P)[A, B C]
CCGraph(V,C,P)[A B, C]
Graphically:
Beta: |
|
= |
|
Eta: |
|
= |
|
Naturality: |
|
= |
|
The graphical semantics is extended with:
[[fn proc P {M} in val]] |
= |
|
[[M N in proc]] |
= |
|
Recursive functions
To allow recursive functions, we just add a new judgement:
For example, with appropriate string and I/O primitives, we can write a
simple `hello' program:
No change is required to the graphical semantics, except to make
edges labelled with types of the form
A1,...,Am B1,...,Bn
traceable.
Initiality
Since we have taken the initial cartesian/monoidal/premonoidal categories
and factored them by equations for the closed structure, the categories:
CCGraph(V,C,P)
CCGraph(V,C,P)
CCGraph(V,C,P)
form the initial triple of categories:
V
C
P
with:
Thus the
graphical semantics defined above uniquely determines a semantics in
any such triples of categories.
Previous |
Next