Nuprl Definition : fan-realizer
fan-realizer ==
λbar,d. eval k = bar_recursion(λn,s. (d map(s;upto(n)));
λ_,__,___. 1;
λ_,__,e. eval a = e tt in eval b = e ff in if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥) in
<k, λf.outl(int_seg_decide(λn.(d map(f;upto(n)));0;k))>
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
bar_recursion: bar_recursion,
int_seg_decide: int_seg_decide(d;i;j),
bottom: ⊥,
callbyvalue: callbyvalue,
outl: outl(x),
bfalse: ff,
btrue: tt,
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
add: n + m,
natural_number: $n
Definitions occuring in definition :
bar_recursion: bar_recursion,
btrue: tt,
bfalse: ff,
less: if (a) < (b) then c else d,
add: n + m,
callbyvalue: callbyvalue,
bottom: ⊥,
pair: <a, b>,
outl: outl(x),
int_seg_decide: int_seg_decide(d;i;j),
lambda: λx.A[x],
apply: f a,
map: map(f;as),
upto: upto(n),
natural_number: $n
Latex:
fan-realizer ==
\mlambda{}bar,d. eval k = bar\_recursion(\mlambda{}n,s. (d map(s;upto(n)));
\mlambda{}$_{}$,\_$_{}$,\_\_$_\mbackslash{}\000Cff7b}$. 1;
\mlambda{}$_{}$,\_$_{}$,e. eval a = e\000C tt in
eval b = e ff in
if (a) < (b) then 1 + b else (1 + a);
0;\mlambda{}m.eval x = m in
\mbot{}) in
<k, \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(d map(f;upto(n)));0;k))>
Date html generated:
2016_05_15-PM-10_05_19
Last ObjectModification:
2015_09_23-AM-08_22_09
Theory : bar!induction
Home
Index