Nuprl Definition : pi-subst-aux

pi-subst-aux(p) ==
  F(p) where 
  F(0) = λY,s. pizero()  
  F(pre.P) = λY,s. pi_prefix_ind(pre;
                                 pisend(c,v)⇒ picomm(pisend(name-subst(s;c);name-subst(s;v));P1 Y s);
                                 pircv(c,v)⇒ if v ∈b Y)
                                 then let w = maybe-new(v;Y @ pi-names(P)) in
                                       let s' = filter(λp.(¬bname_eq(w;fst(p)));s) in
                                       picomm(pircv(name-subst(s;c);w);P1 [w / Y] [<v, w> / s'])
                                 else let s' = filter(λp.(¬bname_eq(v;fst(p)));s) in
                                          picomm(pircv(name-subst(s;c);v);P1 Y s')
                                 fi )  where  
              P1 = F(P)   
  F(P + Q) = λY,s. pioption(P1 Y s;Q1 Y s) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(P | Q) = λY,s. pipar(P1 Y s;Q1 Y s) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(!P) = λY,s. pirep(P1 Y s) where  
           P1 = F(P)  
  F(new v.R) = λY,s. if v ∈b Y)
                    then let w = maybe-new(v;Y @ pi-names(R)) in
                          let s' = filter(λp.(¬bname_eq(w;fst(p)));s) in
                          pinew(w;R1 [w / Y] [<v, w> / s'])
                    else let s' = filter(λp.(¬bname_eq(v;fst(p)));s) in
                             pinew(v;R1 Y s')
                    fi  where  
                R1 = F(R)


Definitions occuring in Statement :  pi-names: pi-names(p),  pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....),  pinew: pinew(name;body),  pirep: pirep(body),  pipar: pipar(left;right),  pioption: pioption(left;right),  picomm: picomm(pre;body),  pizero: pizero(),  pi_prefix_ind: pi_prefix_ind,  pircv: pircv(chan;var),  pisend: pisend(chan;var),  maybe-new: maybe-new(s;avoid),  name-subst: name-subst(s;x),  name_eq: name_eq(x;y),  name-deq: NameDeq,  deq-member: x ∈b L),  filter: filter(P;l),  append: as @ bs,  cons: [a / b],  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  let: let,  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  pair: <a, b>
FDL editor aliases :  pi-subst-aux
Latex:
pi-subst-aux(p)  ==
    F(p)  where 
    F(0)  =  \mlambda{}Y,s.  pizero()   
    F(pre.P)  =  \mlambda{}Y,s.  pi\_prefix\_ind(pre;
                                                                  pisend(c,v){}\mRightarrow{}  picomm(pisend(name-subst(s;c);name-subst(s;v));P1  Y 
                                                                                                                                                                                            s);
                                                                  pircv(c,v){}\mRightarrow{}  if  v  \mmember{}\msubb{}  Y)
                                                                  then  let  w  =  maybe-new(v;Y  @  pi-names(P))  in
                                                                              let  s'  =  filter(\mlambda{}p.(\mneg{}\msubb{}name\_eq(w;fst(p)));s)  in
                                                                              picomm(pircv(name-subst(s;c);w);P1  [w  /  Y]  [<v,  w>  /  s'])
                                                                  else  let  s'  =  filter(\mlambda{}p.(\mneg{}\msubb{}name\_eq(v;fst(p)));s)  in
                                                                                    picomm(pircv(name-subst(s;c);v);P1  Y  s')
                                                                  fi  )    where   
                            P1  =  F(P)     
    F(P  +  Q)  =  \mlambda{}Y,s.  pioption(P1  Y  s;Q1  Y  s)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(P  |  Q)  =  \mlambda{}Y,s.  pipar(P1  Y  s;Q1  Y  s)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(!P)  =  \mlambda{}Y,s.  pirep(P1  Y  s)  where   
                      P1  =  F(P)   
    F(new  v.R)  =  \mlambda{}Y,s.  if  v  \mmember{}\msubb{}  Y)
                                        then  let  w  =  maybe-new(v;Y  @  pi-names(R))  in
                                                    let  s'  =  filter(\mlambda{}p.(\mneg{}\msubb{}name\_eq(w;fst(p)));s)  in
                                                    pinew(w;R1  [w  /  Y]  [<v,  w>  /  s'])
                                        else  let  s'  =  filter(\mlambda{}p.(\mneg{}\msubb{}name\_eq(v;fst(p)));s)  in
                                                          pinew(v;R1  Y  s')
                                        fi    where   
                                R1  =  F(R)


Date html generated: 2015_07_23-AM-11_33_37
Last ObjectModification: 2012_08_30-PM-01_19_13

Home Index