### 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