{ 
[A:{A:
'| 
A} ]. [dfps:DataflowProgram(A) List]. [B:{B:Type|
valueall-type(B)} ].
[G:tuple-type(map(
dfp.bag(df-program-type(dfp));dfps)) 
bag(B) bag(B)].
[halt:tuple-type(map(dfp.(Top?);map(dfp.df-program-type(dfp);dfps))) 
].
better-feedback-dataflow(||dfps||;
k.map(dfp.df-program-meaning(dfp);dfps)[k];
g.(G tuple(||dfps||;i.g i));{};b.
null(b))
= df-program-meaning(feedback-df-prog(B;G;halt;dfps))
supposing feedback-df-halt(G;map(dfp.df-program-type(dfp);dfps);B;halt) }
{ Proof }
Definitions occuring in Statement :
feedback-df-halt: feedback-df-halt(G;L;B;halt),
feedback-df-prog: feedback-df-prog(B;G;halt;dfps),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
dataflow: dataflow(A;B),
select: l[i],
map: map(f;as),
length: ||as||,
null: null(as),
bnot: b,
bool: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
squash: T,
unit: Unit,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
union: left + right,
list: type List,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T),
tuple: tuple(n;i.F[i]),
tuple-type: tuple-type(L),
valueall-type: valueall-type(T)
Lemmas :
dataflow-program_wf,
feedback-df-halt_wf,
map_wf,
bag_wf,
dataflow_wf,
tuple-type_wf,
unit_wf,
top_wf,
bool_wf,
valueall-type_wf,
squash_wf,
df-program-type_wf,
member_wf,
feedback-prog-meaning,
empty-bag_wf,
map-map
\mforall{}[A:\{A:\mBbbU{}'| \mdownarrow{}A\} ]. \mforall{}[dfps:DataflowProgram(A) List]. \mforall{}[B:\{B:Type| valueall-type(B)\} ].
\mforall{}[G:tuple-type(map(\mlambda{}dfp.bag(df-program-type(dfp));dfps)) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)].
\mforall{}[halt:tuple-type(map(\mlambda{}dfp.(Top?);map(\mlambda{}dfp.df-program-type(dfp);dfps))) {}\mrightarrow{} \mBbbB{}].
better-feedback-dataflow(||dfps||;\mlambda{}k.map(\mlambda{}dfp.df-program-meaning(dfp);dfps)[k];
\mlambda{}g.(G tuple(||dfps||;i.g i));\{\};b.\mneg{}\msubb{}null(b))
= df-program-meaning(feedback-df-prog(B;G;halt;dfps))
supposing feedback-df-halt(G;map(\mlambda{}dfp.df-program-type(dfp);dfps);B;halt)
Date html generated:
2011_08_16-AM-09_41_21
Last ObjectModification:
2011_06_24-PM-05_40_58
Home
Index