Nuprl Definition : pi-trans
pi-trans(l_loc;P)
==r if pizero?(P) then λl,serial,avoid. pi-null-trans()
if pipar?(P) then let Q = pipar-left(P) in let R = pipar-right(P) in pi-bar-trans(l_loc;Q;R;λp.pi-trans(l_loc;p))
if pirep?(P) then let Q = pirep-body(P) in pi-rep-trans(l_loc;Q;λp.pi-trans(l_loc;p))
if pinew?(P) then let x = pinew-name(P) in let Q = pinew-body(P) in pi-new-trans(x;Q;λp.pi-trans(l_loc;p))
if pioption?(P) then pi-guarded-trans(pi-choices(P);λp.pi-trans(l_loc;p))
if picomm?(P) then pi-guarded-trans(pi-choices(P);λp.pi-trans(l_loc;p))
else λl,serial,avoid. impossible
fi
pi-trans(l_loc;P) ==
fix((λpi-trans,P. if pizero?(P) then λl,serial,avoid. pi-null-trans()
if pipar?(P)
then let Q = pipar-left(P) in
let R = pipar-right(P) in
pi-bar-trans(l_loc;Q;R;λp.(pi-trans p))
if pirep?(P) then let Q = pirep-body(P) in pi-rep-trans(l_loc;Q;λp.(pi-trans p))
if pinew?(P) then let x = pinew-name(P) in let Q = pinew-body(P) in pi-new-trans(x;Q;λp.(pi-trans p))
if pioption?(P) then pi-guarded-trans(pi-choices(P);λp.(pi-trans p))
if picomm?(P) then pi-guarded-trans(pi-choices(P);λp.(pi-trans p))
else λl,serial,avoid. impossible
fi ))
P
Definitions occuring in Statement :
pi-guarded-trans: pi-guarded-trans(compList;g),
pi-null-trans: pi-null-trans(),
pi-new-trans: pi-new-trans(x;P;g),
pi-rep-trans: pi-rep-trans(l_loc;P;g),
pi-bar-trans: pi-bar-trans(l_loc;P;Q;g),
pi-choices: pi-choices(t),
pinew-body: pinew-body(v),
pinew-name: pinew-name(v),
pinew?: pinew?(v),
pirep-body: pirep-body(v),
pirep?: pirep?(v),
pipar-right: pipar-right(v),
pipar-left: pipar-left(v),
pipar?: pipar?(v),
pioption?: pioption?(v),
picomm?: picomm?(v),
pizero?: pizero?(v),
ifthenelse: if b then t else f fi ,
let: let,
apply: f a,
fix: fix(F),
lambda: λx.A[x]
FDL editor aliases :
pi-trans
Latex:
pi-trans(l$_{loc}$;P)
==r if pizero?(P) then \mlambda{}l,serial,avoid. pi-null-trans()
if pipar?(P)
then let Q = pipar-left(P) in
let R = pipar-right(P) in
pi-bar-trans(l$_{loc}$;Q;R;\mlambda{}p.pi-trans(l$_{loc}$\000C;p))
if pirep?(P) then let Q = pirep-body(P) in pi-rep-trans(l$_{loc}$;Q;\mlambda{}p.pi-tr\000Cans(l$_{loc}$;p))
if pinew?(P)
then let x = pinew-name(P) in
let Q = pinew-body(P) in
pi-new-trans(x;Q;\mlambda{}p.pi-trans(l$_{loc}$;p))
if pioption?(P) then pi-guarded-trans(pi-choices(P);\mlambda{}p.pi-trans(l$_{loc}$;p)\000C)
if picomm?(P) then pi-guarded-trans(pi-choices(P);\mlambda{}p.pi-trans(l$_{loc}$;p))
else \mlambda{}l,serial,avoid. impossible
fi
Latex:
pi-trans(l$_{loc}$;P) ==
fix((\mlambda{}pi-trans,P. if pizero?(P) then \mlambda{}l,serial,avoid. pi-null-trans()
if pipar?(P)
then let Q = pipar-left(P) in
let R = pipar-right(P) in
pi-bar-trans(l$_{loc}$;Q;R;\mlambda{}p.(pi-trans p))
if pirep?(P) then let Q = pirep-body(P) in pi-rep-trans(l$_{loc}\mbackslash{}\000Cff24;Q;\mlambda{}p.(pi-trans p))
if pinew?(P)
then let x = pinew-name(P) in
let Q = pinew-body(P) in
pi-new-trans(x;Q;\mlambda{}p.(pi-trans p))
if pioption?(P) then pi-guarded-trans(pi-choices(P);\mlambda{}p.(pi-trans p))
if picomm?(P) then pi-guarded-trans(pi-choices(P);\mlambda{}p.(pi-trans p))
else \mlambda{}l,serial,avoid. impossible
fi ))
P
Date html generated:
2015_07_23-AM-11_59_29
Last ObjectModification:
2013_10_04-AM-01_00_06
Home
Index