Nuprl Definition : pRun2

pRun2(S0;env;nat2msg;loc2msg;t) ==
  Y 
  (λpRun2,t. if (t =z 0)
            then eval S = norm-system S0 in
                 [<inr ⋅ , S>]
            else eval r = pRun2 (t - 1) in
                 eval nxt = let info,S = let n,m,nm = env t (λi.r[i]) in 
                            do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm) 
                            in eval info' = norm-runinfo(info) in
                               eval S' = norm-system S in
                                 <info', S'> in
                   r @ [nxt]
            fi ) 
  t


Definitions occuring in Statement :  norm-runinfo: norm-runinfo(info),  do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),  norm-system: norm-system,  last: last(L),  select: L[n],  append: as @ bs,  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  it: ⋅,  spreadn: spread3,  pi2: snd(t),  ycomb: Y,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  subtract: n - m,  natural_number: $n
FDL editor aliases :  pRun2
Latex:
pRun2(S0;env;nat2msg;loc2msg;t)  ==
    Y 
    (\mlambda{}pRun2,t.  if  (t  =\msubz{}  0)
                        then  eval  S  =  norm-system  S0  in
                                  [<inr  \mcdot{}  ,  S>]
                        else  eval  r  =  pRun2  (t  -  1)  in
                                  eval  nxt  =  let  info,S  =  let  n,m,nm  =  env  t  (\mlambda{}i.r[i])  in 
                                                        do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm) 
                                                        in  eval  info'  =  norm-runinfo(info)  in
                                                              eval  S'  =  norm-system  S  in
                                                                  <info',  S'>  in
                                      r  @  [nxt]
                        fi  ) 
    t


Date html generated: 2015_07_23-AM-11_10_04
Last ObjectModification: 2012_02_25-PM-03_40_27

Home Index