Nuprl Definition : global-eo

A list of ⌜Id × Info⌝ pairs defines a global ordering of events.
We can construct an event-ordering that agrees with the given global ordering.⋅

global-eo(L) ==
  mk-extended-eo(type: ℕ||L||;
                 domain: λn.tt;
                 loc: λn.(fst(L[n]));
                 info: λn.(snd(L[n]));
                 causal: λe1,e2. e1 < e2;
                 local: λe1,e2. e1 <z e2;
                 pred: λn.eval i = fst(L[n]) in
                          eval z = last_index(firstn(n;L);p.fst(p) = i) in
                            if (z =_z 0) then n else z - 1 fi ;
                 rank: λn.n)

Definitions occuring in Statement : mk-extended-eo: mk-extended-eo, eq_id: a = b, firstn: firstn(n;as), select: L[n], length: ||as||, int_seg: {i..j^-}, callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , lt_int: i <z j, eq_int: (i =_z j), btrue: tt, less_than: a < b, pi1: fst(t), pi2: snd(t), lambda: λx.A[x], subtract: n - m, natural_number: $n, last_index: last_index(L;x.P[x])
FDL editor aliases : global-eo

Latex:
global-eo(L) == mk-extended-eo(type: \mBbbN{}||L||; domain: \mlambda{}n.tt; loc: \mlambda{}n.(fst(L[n])); info: \mlambda{}n.(snd(L[n])); causal: \mlambda{}e1,e2. e1 < e2; local: \mlambda{}e1,e2. e1 <z e2; pred: \mlambda{}n.eval i = fst(L[n]) in eval z = last\_index(firstn(n;L);p.fst(p) = i) in if (z =\msubz{} 0) then n else z - 1 fi ; rank: \mlambda{}n.n) Date html generated: 2016_05_17-PM-03_27_51 Last ObjectModification: 2014_07_23-PM-00_05_56 Theory : event-ordering Home Index