---

pi-subst-aux(p) ==
  F(p) where 
  F(0) = Y,s.0  
  F(pre.P) = Y,s.
              G(pre) where   
              G(c<v>) = name-subst(s;c)<name-subst(s;v)>.P1 Y s  
              G(c?(v)) = if deq-member(NameDeq;v;Y)
                         then let w = maybe-new(v;Y @ pi-names(P)) in
                               let s' = filter(p.(name_eq(w;fst(p)));s) in
                               name-subst(s;c)?(w).P1 [w / Y] [<v, w> / s']
                         else let s' = filter(p.(name_eq(v;fst(p)));s) in
                                  name-subst(s;c)?(v).P1 Y s'
                         fi  where  
              P1 = F(P)   
  F(P + Q) = Y,s.(P1 Y s + Q1 Y s) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(P | Q) = Y,s.(P1 Y s | Q1 Y s) where  
              P1 = F(P)  
              Q1 = F(Q)  
  F(!P) = Y,s.!P1 Y s where  
           P1 = F(P)  
  F(new v.R) = Y,s.
                if deq-member(NameDeq;v;Y)
                then let w = maybe-new(v;Y @ pi-names(R)) in
                      let s' = filter(p.(name_eq(w;fst(p)));s) in
                      (new w. R1 [w / Y] [<v, w> / s'])
                else let s' = filter(p.(name_eq(v;fst(p)));s) in
                         (new v. R1 Y s')
                fi  where  
                R1 = F(R)

---

Definitions :  pi_term_ind: pi_term_ind,  pizero: 0,  pi_prefix_ind: pi_prefix_ind,  pisend: chan<val>,  picomm: pre.body,  pircv: chan?(var),  name-subst: name-subst(s;x),  pioption: (left + right),  pipar: (left | right),  pirep: !body,  ifthenelse: if b then t else f fi ,  deq-member: deq-member(eq;x;L),  name-deq: NameDeq,  maybe-new: maybe-new(s;avoid),  append: as @ bs,  pi-names: pi-names(p),  cons: [car / cdr],  pair: <a, b>,  let: let,  filter: filter(P;l),  lambda: x.A[x],  bnot: b,  name_eq: name_eq(x;y),  pi1: fst(t),  pinew: (new name. body),  apply: f a
FDL editor aliases :  pi-subst-aux

---

pi-subst-aux(p)  ==
    F(p)  where 
    F(0)  =  \mlambda{}Y,s.0   
    F(pre.P)  =  \mlambda{}Y,s.
                            G(pre)  where     
                            G(c<v>)  =  name-subst(s;c)<name-subst(s;v)>.P1  Y  s   
                            G(c?(v))  =  if  deq-member(NameDeq;v;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
                                                              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
                                                                    name-subst(s;c)?(v).P1  Y  s'
                                                  fi    where   
                            P1  =  F(P)     
    F(P  +  Q)  =  \mlambda{}Y,s.(P1  Y  s  +  Q1  Y  s)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(P  |  Q)  =  \mlambda{}Y,s.(P1  Y  s  |  Q1  Y  s)  where   
                            P1  =  F(P)   
                            Q1  =  F(Q)   
    F(!P)  =  \mlambda{}Y,s.!P1  Y  s  where   
                      P1  =  F(P)   
    F(new  v.R)  =  \mlambda{}Y,s.
                                if  deq-member(NameDeq;v;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
                                            (new  w.  R1  [w  /  Y]  [<v,  w>  /  s'])
                                else  let  s'  =  filter(\mlambda{}p.(\mneg{}\msubb{}name\_eq(v;fst(p)));s)  in
                                                  (new  v.  R1  Y  s')
                                fi    where   
                                R1  =  F(R)


Date html generated: 2010_08_27-PM-08_41_36
Last ObjectModification: 2010_03_10-PM-05_21_28

Home Index