Nuprl Definition : list-eo

Given single location, i, and a ⌈L ∈ Info List⌉we can construct an event
ordering where the info associated with the events is exactly L.
The events are the indexes into and both local and causal ordering are <.⋅

list-eo(L;i) ==
  mk-extended-eo(type: ℕ;
                 domain: λn.n <||L||;
                 loc: λe.i;
                 info: λn.if n <||L|| then L[n] else hd(L) fi ;
                 causal: λe1,e2. e1 < e2;
                 local: λe1,e2. e1 <e2;
                 pred: λe.if (e =z 0) then else fi ;
                 rank: λe.e)

Definitions occuring in Statement :  mk-extended-eo: mk-extended-eo select: L[n] hd: hd(l) length: ||as|| nat: ifthenelse: if then else fi  lt_int: i <j eq_int: (i =z j) less_than: a < b lambda: λx.A[x] subtract: m natural_number: $n
FDL editor aliases :  list-eo

list-eo(L;i)  ==
    mk-extended-eo(type:  \mBbbN{};
                                  domain:  \mlambda{}n.n  <z  ||L||;
                                  loc:  \mlambda{}e.i;
                                  info:  \mlambda{}n.if  n  <z  ||L||  then  L[n]  else  hd(L)  fi  ;
                                  causal:  \mlambda{}e1,e2.  e1  <  e2;
                                  local:  \mlambda{}e1,e2.  e1  <z  e2;
                                  pred:  \mlambda{}e.if  (e  =\msubz{}  0)  then  0  else  e  -  1  fi  ;
                                  rank:  \mlambda{}e.e)

Date html generated: 2015_07_21-PM-04_28_50
Last ObjectModification: 2014_07_23-PM-00_02_38

Home Index