Nuprl Definition : pi-guarded-aux

pi-guarded-aux(compList;g)
==r λl,serial,avoid,m. if pDVmsg?(m)
                      then let val = pDVmsg-val(m) in
                            let i = pDVmsg-index(m) in
                            if i <z ||compList||
                            then let pre_i,P_i = compList[i] 
                                 in let P' = ... in
                                        <g P' l serial avoid ∪ pi-names(P'), make-lg([<l, mk-tagged("msg";pDVfire())>])>
                            else <pi-guarded-aux(compList;g) l serial avoid, make-lg([])>
                            fi 
                      else <pi-guarded-aux(compList;g) l serial avoid, make-lg([])>
                      fi 
pi-guarded-aux(compList;g) ==
  fix((λpi-guarded-aux,l,serial,avoid,m. if pDVmsg?(m)
                                        then let val = pDVmsg-val(m) in
                                              let i = pDVmsg-index(m) in
                                              if i <z ||compList||
                                              then let pre_i,P_i = compList[i] 
                                                   in let P' = if pircv?(pre_i)
                                                               then pi-simple-subst(val;pircv-var(pre_i);P_i)
                                                               else P_i
                                                               fi  in
                                                          <g P' l serial avoid ∪ pi-names(P')
                                                          , make-lg([<l, mk-tagged("msg";pDVfire())>])
                                                          >
                                              else <pi-guarded-aux l serial avoid, make-lg([])>
                                              fi 
                                        else <pi-guarded-aux l serial avoid, make-lg([])>
                                        fi ))


Definitions occuring in Statement :  pDVmsg-index: pDVmsg-index(x),  pDVmsg-val: pDVmsg-val(x),  pDVmsg?: pDVmsg?(x),  pDVfire: pDVfire(),  pi-simple-subst: pi-simple-subst(t;x;P),  pi-names: pi-names(p),  pircv-var: pircv-var(v),  pircv?: pircv?(v),  make-lg: make-lg(L),  name-deq: NameDeq,  l-union: as ∪ bs,  select: L[n],  length: ||as||,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  let: let,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  token: "$token",  mk-tagged: mk-tagged(tg;x)
FDL editor aliases :  pi-guarded-aux
Latex:

pi-guarded-aux(compList;g)
==r  \mlambda{}l,serial,avoid,m.  if  pDVmsg?(m)
                                            then  let  val  =  pDVmsg-val(m)  in
                                                        let  i  =  pDVmsg-index(m)  in
                                                        if  i  <z  ||compList||
                                                        then  let  pre$_{i}$,P$_{i}$  =  com\000CpList[i] 
                                                                  in  let  P'  =  if  pircv?(pre$_{i}$)
                                                                                          then  pi-simple-subst(val;pircv-var(pre$_{i\mbackslash{}\000Cff7d$);P$_{i}$)
                                                                                          else  P$_{i}$
                                                                                          fi    in
                                                                                <g  P'  l  serial  avoid  \mcup{}  pi-names(P')
                                                                                ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                                                >
                                                        else  <pi-guarded-aux(compList;g)  l  serial  avoid,  make-lg([])>
                                                        fi 
                                            else  <pi-guarded-aux(compList;g)  l  serial  avoid,  make-lg([])>
                                            fi 

Latex:
pi-guarded-aux(compList;g)  ==
    fix((\mlambda{}pi-guarded-aux,l,serial,avoid,m.  if  pDVmsg?(m)
                                                                                then  let  val  =  pDVmsg-val(m)  in
                                                                                            let  i  =  pDVmsg-index(m)  in
                                                                                            if  i  <z  ||compList||
                                                                                            then  let  pre$_{i}$,P$_\mbackslash{}ff7\000Cbi}$  =  compList[i] 
                                                                                                      in  let  P'  =  if  pircv?(pre$_{i}\mbackslash{}ff\000C24)
                                                                                                                              then  pi-simple-subst(val;...;P$\mbackslash{}f\000Cf5f{i}$)
                                                                                                                              else  P$_{i}$
                                                                                                                              fi    in
                                                                                                                    <g  P'  l  serial  avoid  \mcup{}  pi-names(P')
                                                                                                                    ,  make-lg([<l,  mk-tagged("msg";pDVfire())>\000C])
                                                                                                                    >
                                                                                            else  <pi-guarded-aux  l  serial  avoid,  make-lg([])>
                                                                                            fi 
                                                                                else  <pi-guarded-aux  l  serial  avoid,  make-lg([])>
                                                                                fi  ))


Date html generated: 2015_07_23-AM-11_59_20
Last ObjectModification: 2013_10_04-AM-00_19_16

Home Index