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