Nuprl Definition : modelEval

modelEval(exname;M;n)
==r let consts,funs = M 
    in case apply-alist(IntDeq;funs;n)
        of inl(lst) =>
        λi.if i is an integer then case apply-alist(IntDeq;lst;i)
            of inl(j) =>
            modelEval(exname;M;j)
            | inr(x) =>
            exception(exname; <n, i>)
           else exception(exname; <n, i>)
        | inr(x) =>
        case apply-alist(IntDeq;consts;n)
         of inl(x) =>
         let lbl,i,j = x in 
         if lbl =a "function" then λx.exception(<exname, n, x>)
         if lbl =a "pair" then <modelEval(exname;M;i), modelEval(exname;M;j)>
         if lbl =a "dpair" then <i, modelEval(exname;M;j)>
         if lbl =a "inl" then inl modelEval(exname;M;i)
         if lbl =a "inr" then inr modelEval(exname;M;i) 
         if lbl =a "const" then λx.modelEval(exname;M;i)
         else exception(exname; n)
         fi 
         | inr(x) =>
         exception(exname; n)
modelEval(exname;M;n) ==
  fix((λmodelEval,n. let consts,funs = M 
                     in case apply-alist(IntDeq;funs;n)
                         of inl(lst) =>
                         λi.if i is an integer then case apply-alist(IntDeq;lst;i)
                             of inl(j) =>
                             modelEval j
                             | inr(x) =>
                             exception(exname; <n, i>)
                            else exception(exname; <n, i>)
                         | inr(x) =>
                         case apply-alist(IntDeq;consts;n)
                          of inl(x) =>
                          let lbl,i,j = x in 
                          if lbl =a "function" then λx.(exception(exname; <n, x>))
                          if lbl =a "pair" then <modelEval i, modelEval j>
                          if lbl =a "dpair" then <i, modelEval j>
                          if lbl =a "inl" then inl (modelEval i)
                          if lbl =a "inr" then inr (modelEval i) 
                          if lbl =a "const" then λx.(modelEval i)
                          else exception(exname; n)
                          fi 
                          | inr(x) =>
                          exception(exname; n))) 
  n


Definitions occuring in Statement :  apply-alist: apply-alist(eq;L;x),  int-deq: IntDeq,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  spreadn: spread3,  isint: isint def,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  token: "$token"
Definitions occuring in definition :  fix: fix(F),  spread: spread def,  isint: isint def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply-alist: apply-alist(eq;L;x),  int-deq: IntDeq,  spreadn: spread3,  pair: <a, b>,  inl: inl x,  inr: inr x ,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  token: "$token",  lambda: λx.A[x],  apply: f a
FDL editor aliases :  modelEval
Latex:
modelEval(exname;M;n)
==r  let  consts,funs  =  M 
        in  case  apply-alist(IntDeq;funs;n)
                of  inl(lst)  =>
                \mlambda{}i.if  i  is  an  integer  then  case  apply-alist(IntDeq;lst;i)
                        of  inl(j)  =>
                        modelEval(exname;M;j)
                        |  inr(x)  =>
                        exception(exname;  <n,  i>)
                      else  exception(exname;  <n,  i>)
                |  inr(x)  =>
                case  apply-alist(IntDeq;consts;n)
                  of  inl(x)  =>
                  let  lbl,i,j  =  x  in 
                  if  lbl  =a  "function"  then  \mlambda{}x.exception(<exname,  n,  x>)
                  if  lbl  =a  "pair"  then  <modelEval(exname;M;i),  modelEval(exname;M;j)>
                  if  lbl  =a  "dpair"  then  <i,  modelEval(exname;M;j)>
                  if  lbl  =a  "inl"  then  inl  modelEval(exname;M;i)
                  if  lbl  =a  "inr"  then  inr  modelEval(exname;M;i) 
                  if  lbl  =a  "const"  then  \mlambda{}x.modelEval(exname;M;i)
                  else  exception(exname;  n)
                  fi 
                  |  inr(x)  =>
                  exception(exname;  n)
Latex:
modelEval(exname;M;n)  ==
    fix((\mlambda{}modelEval,n.  let  consts,funs  =  M 
                                          in  case  apply-alist(IntDeq;funs;n)
                                                  of  inl(lst)  =>
                                                  \mlambda{}i.if  i  is  an  integer  then  case  apply-alist(IntDeq;lst;i)
                                                          of  inl(j)  =>
                                                          modelEval  j
                                                          |  inr(x)  =>
                                                          exception(exname;  <n,  i>)
                                                        else  exception(exname;  <n,  i>)
                                                  |  inr(x)  =>
                                                  case  apply-alist(IntDeq;consts;n)
                                                    of  inl(x)  =>
                                                    let  lbl,i,j  =  x  in 
                                                    if  lbl  =a  "function"  then  \mlambda{}x.(exception(exname;  <n,  x>))
                                                    if  lbl  =a  "pair"  then  <modelEval  i,  modelEval  j>
                                                    if  lbl  =a  "dpair"  then  <i,  modelEval  j>
                                                    if  lbl  =a  "inl"  then  inl  (modelEval  i)
                                                    if  lbl  =a  "inr"  then  inr  (modelEval  i) 
                                                    if  lbl  =a  "const"  then  \mlambda{}x.(modelEval  i)
                                                    else  exception(exname;  n)
                                                    fi 
                                                    |  inr(x)  =>
                                                    exception(exname;  n))) 
    n


Date html generated: 2016_05_15-PM-10_32_30
Last ObjectModification: 2015_09_24-PM-08_30_16

Theory : minimal-first-order-logic


Home Index