Nuprl Definition : compute-in-context

compute-in-context(constants;functions;t) ==
  fix((λ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 (λ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) =>
                                 t
                                else t
                                otherwise x.t)
                                | inr(z) =>
                                t
                              otherwise x.x)))
  t

Definitions occuring in Statement : apply-alist: apply-alist(eq;L;x), int-deq: IntDeq, isint: isint def, apply: f a, fix: fix(F), lambda: λx.A[x], decide: case b 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) => t else t otherwise x.t) | inr(z) => t otherwise x.x))) t Date html generated: 2015_07_17-AM-07_57_21 Last ObjectModification: 2012_12_06-PM-05_33_32 Home Index