17291
|
1 |
(* $Id$ *)
|
|
2 |
|
2570
|
3 |
(* Specification of the following loop back device
|
|
4 |
|
|
5 |
|
17291
|
6 |
g
|
2570
|
7 |
--------------------
|
|
8 |
| ------- |
|
|
9 |
x | | | | y
|
17291
|
10 |
------|---->| |------| ----->
|
2570
|
11 |
| z | f | z |
|
|
12 |
| -->| |--- |
|
|
13 |
| | | | | |
|
|
14 |
| | ------- | |
|
|
15 |
| | | |
|
|
16 |
| <-------------- |
|
17291
|
17 |
| |
|
2570
|
18 |
--------------------
|
|
19 |
|
|
20 |
|
|
21 |
First step: Notation in Agent Network Description Language (ANDL)
|
|
22 |
-----------------------------------------------------------------
|
|
23 |
|
|
24 |
agent f
|
17291
|
25 |
input channel i1:'b i2: ('b,'c) tc
|
|
26 |
output channel o1:'c o2: ('b,'c) tc
|
2570
|
27 |
is
|
17291
|
28 |
Rf(i1,i2,o1,o2) (left open in the example)
|
2570
|
29 |
end f
|
|
30 |
|
|
31 |
agent g
|
17291
|
32 |
input channel x:'b
|
|
33 |
output channel y:'c
|
2570
|
34 |
is network
|
17291
|
35 |
<y,z> = f$<x,z>
|
2570
|
36 |
end network
|
|
37 |
end g
|
|
38 |
|
|
39 |
|
|
40 |
Remark: the type of the feedback depends at most on the types of the input and
|
|
41 |
output of g. (No type miracles inside g)
|
|
42 |
|
|
43 |
Second step: Translation of ANDL specification to HOLCF Specification
|
|
44 |
---------------------------------------------------------------------
|
|
45 |
|
|
46 |
Specification of agent f ist translated to predicate is_f
|
|
47 |
|
17291
|
48 |
is_f :: ('b stream * ('b,'c) tc stream ->
|
|
49 |
'c stream * ('b,'c) tc stream) => bool
|
2570
|
50 |
|
17291
|
51 |
is_f f = !i1 i2 o1 o2.
|
|
52 |
f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
|
2570
|
53 |
|
|
54 |
Specification of agent g is translated to predicate is_g which uses
|
|
55 |
predicate is_net_g
|
|
56 |
|
|
57 |
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
|
17291
|
58 |
'b stream => 'c stream => bool
|
2570
|
59 |
|
17291
|
60 |
is_net_g f x y =
|
|
61 |
? z. <y,z> = f$<x,z> &
|
|
62 |
!oy hz. <oy,hz> = f$<x,hz> --> z << hz
|
2570
|
63 |
|
|
64 |
|
|
65 |
is_g :: ('b stream -> 'c stream) => bool
|
|
66 |
|
10835
|
67 |
is_g g = ? f. is_f f & (!x y. g$x = y --> is_net_g f x y
|
17291
|
68 |
|
2570
|
69 |
Third step: (show conservativity)
|
|
70 |
-----------
|
|
71 |
|
|
72 |
Suppose we have a model for the theory TH1 which contains the axiom
|
|
73 |
|
17291
|
74 |
? f. is_f f
|
2570
|
75 |
|
|
76 |
In this case there is also a model for the theory TH2 that enriches TH1 by
|
|
77 |
axiom
|
|
78 |
|
17291
|
79 |
? g. is_g g
|
2570
|
80 |
|
|
81 |
The result is proved by showing that there is a definitional extension
|
|
82 |
that extends TH1 by a definition of g.
|
|
83 |
|
|
84 |
|
|
85 |
We define:
|
|
86 |
|
17291
|
87 |
def_g g =
|
|
88 |
(? f. is_f f &
|
|
89 |
g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )
|
|
90 |
|
2570
|
91 |
Now we prove:
|
|
92 |
|
17291
|
93 |
(? f. is_f f ) --> (? g. is_g g)
|
2570
|
94 |
|
|
95 |
using the theorems
|
|
96 |
|
17291
|
97 |
loopback_eq) def_g = is_g (real work)
|
2570
|
98 |
|
17291
|
99 |
L1) (? f. is_f f ) --> (? g. def_g g) (trivial)
|
2570
|
100 |
|
|
101 |
*)
|
|
102 |
|
17291
|
103 |
theory Focus_ex
|
|
104 |
imports Stream
|
|
105 |
begin
|
2570
|
106 |
|
17291
|
107 |
typedecl ('a, 'b) tc
|
|
108 |
arities tc:: (pcpo, pcpo) pcpo
|
2570
|
109 |
|
|
110 |
consts
|
|
111 |
|
|
112 |
is_f ::
|
|
113 |
"('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
|
|
114 |
is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
|
17291
|
115 |
'b stream => 'c stream => bool"
|
2570
|
116 |
is_g :: "('b stream -> 'c stream) => bool"
|
|
117 |
def_g :: "('b stream -> 'c stream) => bool"
|
17291
|
118 |
Rf ::
|
2570
|
119 |
"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
|
|
120 |
|
|
121 |
defs
|
|
122 |
|
17291
|
123 |
is_f: "is_f f == (!i1 i2 o1 o2.
|
|
124 |
f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
|
2570
|
125 |
|
17291
|
126 |
is_net_g: "is_net_g f x y == (? z.
|
|
127 |
<y,z> = f$<x,z> &
|
|
128 |
(!oy hz. <oy,hz> = f$<x,hz> --> z << hz))"
|
2570
|
129 |
|
17291
|
130 |
is_g: "is_g g == (? f.
|
|
131 |
is_f f &
|
|
132 |
(!x y. g$x = y --> is_net_g f x y))"
|
2570
|
133 |
|
|
134 |
|
17291
|
135 |
def_g: "def_g g == (? f.
|
|
136 |
is_f f &
|
|
137 |
g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))"
|
|
138 |
|
|
139 |
ML {* use_legacy_bindings (the_context ()) *}
|
2570
|
140 |
|
|
141 |
end
|