Nuprl Definition : subst-exc

subst-exc(e;t)
==r eval x = t in
    if x is lambda then λz.subst-exc(e;x z) otherwise if x is a pair then let a,b = x 
                                                                          in eval a' = subst-exc(e;a) in
                                                                             eval b' = subst-exc(e;b) in
                                                                               <a', b'>
                                                      otherwise if x is inl then eval y = subst-exc(e;outl(x)) in
                                                                                 inl y
                                                                else if x is inr then eval y = subst-exc(e;outr(x)) in
                                                                                      inr y 
                                                                     else x?e:v.⊥
subst-exc(e;t) ==
  fix((λsubst-exc,t. eval x = t in
                     if x is lambda then λz.(subst-exc (x z)) otherwise if x is a pair then let a,b = x 
                                                                                            in eval a' = subst-exc a in
                                                                                               eval b' = subst-exc b in
                                                                                                 <a', b'>
                                                                        otherwise if x is inl then eval y = subst-exc 
                                                                                                            outl(x) in
                                                                                                   inl y
                                                                                  else if x is inr
                                                                                       eval y = subst-exc outr(x) in
                                                                                       inr y 
                                                                                       else x?e:v.⊥)) 
  t


Definitions occuring in Statement :  callbyvalue: callbyvalue,  outr: outr(x),  outl: outl(x),  ispair: if z is a pair then a otherwise b,  islambda: if z is lambda then a otherwise b,  isinr: isinr def,  isinl: isinl def,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x
Definitions occuring in definition :  fix: fix(F),  islambda: if z is lambda then a otherwise b,  lambda: λx.A[x],  ispair: if z is a pair then a otherwise b,  spread: spread def,  pair: <a, b>,  isinl: isinl def,  outl: outl(x),  inl: inl x,  isinr: isinr def,  callbyvalue: callbyvalue,  apply: f a,  outr: outr(x),  inr: inr x 
FDL editor aliases :  subst-exc
Latex:
subst-exc(e;t)
==r  eval  x  =  t  in
        if  x  is  lambda  then  \mlambda{}z.subst-exc(e;x  z)
        otherwise  if  x  is  a  pair  then  let  a,b  =  x 
                                                                    in  eval  a'  =  subst-exc(e;a)  in
                                                                          eval  b'  =  subst-exc(e;b)  in
                                                                              <a',  b'>
                            otherwise  if  x  is  inl  then  eval  y  =  subst-exc(e;outl(x))  in
                                                                                  inl  y
                                                else  if  x  is  inr  then  eval  y  =  subst-exc(e;outr(x))  in
                                                                                            inr  y 
                                                          else  x?e:v.\mbot{}
Latex:
subst-exc(e;t)  ==
    fix((\mlambda{}subst-exc,t.  eval  x  =  t  in
                                          if  x  is  lambda  then  \mlambda{}z.(subst-exc  (x  z))
                                          otherwise  if  x  is  a  pair  then  let  a,b  =  x 
                                                                                                      in  eval  a'  =  subst-exc  a  in
                                                                                                            eval  b'  =  subst-exc  b  in
                                                                                                                <a',  b'>
                                                              otherwise  if  x  is  inl  then  eval  y  =  subst-exc  outl(x)  in
                                                                                                                    inl  y
                                                                                  else  if  x  is  inr  then  eval  y  =  subst-exc  outr(x)  in
                                                                                                                              inr  y 
                                                                                            else  x?e:v.\mbot{})) 
    t


Date html generated: 2017_02_20-AM-10_46_09
Last ObjectModification: 2017_01_25-PM-04_07_43

Theory : call!by!value_1


Home Index