Nuprl Lemma : feedback-prog-meaning
[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))) 
]. [init:bag(B)].
better-feedback-dataflow(||dfps||;k.map(dfp.df-program-meaning(dfp);dfps)[k];
g.(G tuple(||dfps||;i.g i));init;b.
null(b))
= df-program-meaning(G|dfps|
feedback: init
halt: halt)
supposing feedback-df-halt(G;map(dfp.df-program-type(dfp);dfps);B;halt)
Proof not projected
Definitions occuring in Statement :
feedback-df-halt: feedback-df-halt(G;L;B;halt),
feedback-prog: feedback-prog,
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,
bag: bag(T),
tuple: tuple(n;i.F[i]),
tuple-type: tuple-type(L),
valueall-type: valueall-type(T)
Definitions :
suptype: suptype(S; T),
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
df-program-meaning: df-program-meaning(dfp),
bnot: b,
feedback-prog: feedback-prog,
spreadn: spread4,
ifthenelse: if b then t else f fi ,
pi2: snd(t),
pi1: fst(t),
prop: 
,
all: x:A. B[x],
implies: P 
Q,
so_apply: x[s1;s2],
member: t 
T,
int_seg: {i..j
},
le: A 
B,
lelt: i j < k,
not: A,
false: False,
and: P 
Q,
so_lambda: 
x y.t[x; y],
nat: 
,
so_lambda: x.t[x],
subtype: S 
T,
btrue: tt,
bfalse: ff,
cand: A c B,
compose: f o g,
df-program-statetype: df-program-statetype(dfp),
df-program-type: df-program-type(dfp),
true: True,
has-valueall: has-valueall(a),
squash: T,
unit: Unit,
rev_implies: P 
Q,
iff: P Q,
exposed-bfalse: exposed-bfalse,
isl: isl(x),
exists: 
x:A. B[x],
ycomb: Y,
zip: zip(as;bs),
length: ||as||,
map: map(f;as),
label: ...$L... t,
df-program-in-state: df-program-in-state(dfp;s),
dataflow-out: dataflow-out(df;a),
dfp-meaning-in-state: dfp-meaning-in-state(dfp;x),
null-dataflow: null-dataflow(),
so_apply: x[s],
l_all: (xL.P[x]),
assert: 
b,
bool: ,
uiff: uiff(P;Q),
dataflow-program: DataflowProgram(A),
sq_stable: SqStable(P),
feedback-df-halt: feedback-df-halt(G;L;B;halt),
strict-bag-function: strict-bag-function(G;L;B;S),
it: 
,
has-value: has-value(a),
guard: {T}
Lemmas :
less_than_wf,
nat_wf,
and_wf,
squash_wf,
valueall-type_wf,
feedback-df-halt_wf,
rec-dataflow-equal,
bag_wf,
int_seg_wf,
length_wf,
dataflow_wf,
df-program-type_wf,
select_wf,
tuple-type_wf,
map_wf,
df-program-statetype_wf,
unit_wf2,
eval-parallel-dataflow_wf,
length_wf_nat,
dataflow-program_wf,
null_wf3,
tuple_wf,
select-map,
top_wf,
lelt_wf,
bag-subtype-list,
bool_wf,
eqtt_to_assert,
uiff_transitivity,
equal_wf,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
df-program-meaning_wf,
df-program-state_wf,
non_neg_length,
map_length,
all_wf,
dfp-meaning-in-state_wf,
subtype_rel_list,
dataflow-program-cumulativity,
select-tuple_wf,
le_wf,
better-feedback-dataflow_wf,
null-dataflow_wf,
length-map,
map-map,
empty-bag_wf,
int_inc_real,
real-has-value,
subtype_rel_bag,
subtype_rel_self,
subtype_rel_simple_product,
function-valueall-type,
tuple-type-valueall-type,
it_wf,
ifthenelse_wf,
ap2-tuple_wf,
zip_wf,
pi2_wf,
pi1_wf_top,
subtype_rel-equal,
df-program-type-valueall-type,
bag-valueall-type,
equal-valueall-type,
df-program-statetype-valueall-type,
union-valueall-type,
product-valueall-type,
sq_stable__valueall-type,
map-tuple_wf,
evalall_wf,
eval-parallel-dataflow-property,
l_member_wf,
bfalse_wf,
btrue_wf,
l_all_wf2,
strict-bag-function_wf,
subtype_rel_sum,
subtype_rel_tuple-type,
dataflow-out_wf,
length-map-sq,
select-zip,
length_zip,
true_wf,
tuple-type-subtype-n-tuple,
tuple_wf_ntuple,
ap2-tuple-as-tuple,
map-tuple-tuple,
select-tuple-tuple,
subtype_top,
dataflow-ap_wf,
false_wf,
map-tuple-as-tuple
\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{}]. \mforall{}[init:bag(B)].
better-feedback-dataflow(||dfps||;\mlambda{}k.map(\mlambda{}dfp.df-program-meaning(dfp);dfps)[k];
\mlambda{}g.(G tuple(||dfps||;i.g i));init;b.\mneg{}\msubb{}null(b))
= df-program-meaning(G|dfps|
feedback: init
halt: halt)
supposing feedback-df-halt(G;map(\mlambda{}dfp.df-program-type(dfp);dfps);B;halt)
Date html generated:
2012_01_23-AM-11_59_56
Last ObjectModification:
2011_12_16-PM-12_23_19
Home
Index