Nuprl Definition : compute-in-context

compute-in-context(constants;functions;t) ==
  fix((λcompute-in-context,t. (if is stopped at f,n then
                              case apply-alist(IntDeq;constants;n)
                               of inl(x) =>
                               compute-in-context (f x)
                               inr(z) =>
                               case apply-alist(IntDeq;functions;n)
                                of inl(table) =>
                                (if x.stop(x)) is stopped at g,arg then
                                if compute-in-context arg is an integer
                                case apply-alist(IntDeq;table;compute-in-context arg)
                                 of inl(z) =>
                                 compute-in-context (f x.z))
                                 inr(z) =>
                                else t
                                otherwise x.t)
                                inr(z) =>
                              otherwise x.x))) 

Definitions occuring in Statement :  apply-alist: apply-alist(eq;L;x) int-deq: IntDeq isint: isint def apply: a fix: fix(F) lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y]
FDL editor aliases :  compute-in-context
compute-in-context(constants;functions;t)  ==
    fix((\mlambda{}compute-in-context,t.  (if  t  is  stopped  at  f,n  then
                                                            case  apply-alist(IntDeq;constants;n)
                                                              of  inl(x)  =>
                                                              compute-in-context  (f  x)
                                                              |  inr(z)  =>
                                                              case  apply-alist(IntDeq;functions;n)
                                                                of  inl(table)  =>
                                                                (if  f  (\mlambda{}x.stop(x))  is  stopped  at  g,arg  then
                                                                if  compute-in-context  arg  is  an  integer
                                                                case  apply-alist(IntDeq;table;compute-in-context  arg)
                                                                  of  inl(z)  =>
                                                                  compute-in-context  (f  (\mlambda{}x.z))
                                                                  |  inr(z)  =>
                                                                else  t
                                                                otherwise  x.t)
                                                                |  inr(z)  =>
                                                            otherwise  x.x))) 

Date html generated: 2015_07_17-AM-07_57_21
Last ObjectModification: 2012_12_06-PM-05_33_32

Home Index