Nuprl Definition : pi-rep-trans
pi-rep-trans(l_loc;P;g) ==
λl,serial,avoid. RecProcess(0;s,m.if (s =z 0) ∧b pDVfire?(m) then <1, make-lg([<l_loc, mk-tagged("msg";pDVloc(l))>])>
if (s =z 1) ∧b pDVloc_tag?(m)
then let l1 = pDVloc_tag-id(m) in
let n1 = pDVloc_tag-name(m) in
<0
, lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>;\000C <l, mk-tagged("msg";pDVfire())>]);0;1)
>
else <s, make-lg([])>
fi )
Definitions occuring in Statement :
pDVfire?: pDVfire?(x),
pDVloc_tag-name: pDVloc_tag-name(x),
pDVloc_tag-id: pDVloc_tag-id(x),
pDVloc_tag?: pDVloc_tag?(x),
pDVfire: pDVfire(),
pDVloc: pDVloc(id),
lg-add: lg-add(g;a;b),
make-lg: make-lg(L),
rec-process: RecProcess(s0;s,m.next[s; m]),
cons: [a / b],
nil: [],
band: p ∧b q,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
let: let,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n,
token: "$token",
mk-tagged: mk-tagged(tg;x)
FDL editor aliases :
pi-rep-trans
Latex:
pi-rep-trans(l$_{loc}$;P;g) ==
\mlambda{}l,serial,avoid. RecProcess(0;s,m.if (s =\msubz{} 0) \mwedge{}\msubb{} pDVfire?(m)
then ə, make-lg([<l$_{loc}$, mk-tagged("m\000Csg";pDVloc(l))>])>
if (s =\msubz{} 1) \mwedge{}\msubb{} pDVloc\_tag?(m)
then let l1 = pDVloc\_tag-id(m) in
let n1 = pDVloc\_tag-name(m) in
ɘ
, lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>
<l1, mk-tagged("msg";pDVfire())>
<l, mk-tagged("msg";pDVfire())>]);0;1)
>
else <s, make-lg([])>
fi )
Date html generated:
2015_07_23-AM-11_59_07
Last ObjectModification:
2012_08_30-PM-01_49_55
Home
Index