Nuprl Definition : q-constraints-decider
q-constraints-decider ==
λk.letrec rec(k)=λA.eval z = evalall(A) in
if if k=0 then inl Ax else (inr (λx.Ax) )
then λA.if l-all-decider() A (λxr.q-rel-decider(let x,y = xr in y;let x,y = xr in x 0))
then inl []
else inr (λ%6.Ax)
fi
else λA.case l-exists-decider() evalall(A)
(λxr.case if let x,y = xr in y=0 then inl Ax else (inr (λx.Ax) )
of inl(%2) =>
case if if qeq(let x,y = xr in x k;0) then inl Ax else inr (λx.Ax) fi
then inr (λ%.Ax)
else inl (λ%.Ax)
fi
of inl(%3) =>
inl <%2, %3>
| inr(%4) =>
inr (λ%.let %5,%6 = %
in Ax)
| inr(%3) =>
inr (λ%.let %4,%5 = %
in Ax) )
of inl(%@0) =>
let xr,%10 = let i,%1 = %@0
in <evalall(A)[i], <i, Ax, Ax>, %1>
in let x1,x2 = xr
in let %11,%13,%14 = %10 in
case rec (k - 1)
map(λxr.let x,r = xr
in <λj.((x j) + -((x k/x1 k) * (x1 j))), r>;evalall(A))
of inl(%15) =>
inl (%15 @ [q-linear(k - 1;j.(-1/x1 k) * (x1 j);%15)])
| inr(%16) =>
inr (λ%.Ax)
| inr(%8) =>
case rec (k - 1)
eval A' = evalall(map(λp.let f,r = p
in eval r = r in
eval as = evalall(map(f;[0, k))) in
<λn.if if (n) < (||as||) then inl Ax else (inr Ax )
then as[n]
else f n
fi
, r
>;filter(λa.qeq(let x,y = a in x k;0);evalall(A))
@ concat(map(λa.map(λb.<λj.(((let x,y = a in x k)
* (let x,y = b in x j))
+ -((let x,y = b in x k)
* (let x,y = a in x j)))
, q-rel-lub(let x,y = a
in y;let x,y = b
in y)
>;filter(λc.q_less(let x,y = c
in x
k;0);evalall(A)));
filter(λb.q_less(0;let x,y = b in x k);
evalall(A)))))) in
A'
of inl(%) =>
inl case l-exists-decider() evalall(A)
(λa.if qpositive((let x,y = a in x k) + -(0))
then inl Ax
else inr (λx.Ax)
fi )
of inl(%@0) =>
case l-exists-decider() evalall(A)
(λa.if qpositive(0 + -(let x,y = a in x k)) then inl Ax else inr (λx.Ax) fi )
of inl(%17) =>
let b,%28,%30,%31 = let a,%25,%26 = if if if map(λc.(-((1/let x,y = c in x k))
* q-linear(k - 1;j.let x,y = c
in x
j;%));
filter(λc.q_less(let x,y = c
in x
k;0);
evalall(A))) = Ax then inl Ax
otherwise inr Ax
then inl Ax
else inr Ax
fi
then <0, Ax, λi.Ax>
else let u,v = map(λc.(-((1/let x,y = c in x k))
* q-linear(k - 1;j.let x,y = c in x j;%));
filter(λc.q_less(let x,y = c in x k;0);evalall(A)))
in <accumulate (with value x and list item y):
if eval r' = evalall(x) in
eval s' = evalall(y) in
qpositive(s' + -(r')) ∨bqeq(r';s')
then x
else y
fi
over list:
tl([u / v])
with starting value:
hd([u / v]))
, if if if [u / v] = Ax then inl Ax otherwise inr Ax
then inl Ax
else inr Ax
fi
then Ax
else let u,v = [u / v]
in rec-case(v) of
[] => λ-any.<0, Ax, Ax>
a::L =>
r.λu@0.if if eval r' = evalall(u@0) in
eval s' = evalall(a) in
qpositive(s' + -(r')) ∨bqeq(r';s')
then inl Ax
if if eval r' = evalall(u@0) in
eval s' = evalall(a) in
qpositive(s' + -(r')) ∨bqeq(r';s')
then inl Ax
else inr Ax
fi
then Ax
else inr Ax
fi
then case case case let i,%2,%3 = r u@0 in
if case if i=0 then inl Ax else (inr Ax )
of inl(x) =>
inl x
| inr(x) =>
inr (λx.Ax)
then λ%,%4. (inl Ax)
else λ%,%6. (inr <i - 1, Ax, Ax> )
fi
Ax
Ax
of inl(%9) =>
inl Ax
| inr(%10) =>
inr inr %10
of inl(-any) =>
inl Ax
| inr(-any) =>
inr case -any
of inl(%1) =>
<0, Ax, Ax>
| inr(%2) =>
let i,%4,%5 = %2 in
<i + 1, Ax, Ax>
of inl(%1) =>
<0, Ax, Ax>
| inr(%2) =>
let i,%4,%5 = %2 in
<i + 1, Ax, Ax>
else let i,%4,%5 = r a in
<i + 1, Ax, Ax>
fi
u
fi
, let %7,%8 =
primrec(||[u / v]|| + 1;λn.Ax;
λi,x,n. if if n=(i + 1) - 1 then inl Ax else (inr (λx.Ax) )
then λL,%7,a. if if if L = Ax then inl Ax otherwise inr Ax
then inl Ax
else inr Ax
fi
then Ax
else let u,v = L
in if null(v)
then <λ-any,i. -any, λ-any.(-any 0)>
else let %18,%19 =
let %23,%24 =
let %22,%23 =
x ||v|| v
case case if if (||v||) < (...)
then inl Ax
else (inr ... )
then inr (λ%.Ax)
else inl (λ%.Ax)
fi
of inl(%2) =>
inl <%2, Ax, Ax>
| inr(%3) =>
inr (λ%.let %4,%5 = %
in Ax)
of inl(%13) =>
%13
| inr(%14) =>
Ax
a
in <λ%26.<let %27,%28 = %26
in %27
, let %27,%28 = %26
in %28
>
, λ%26.<let %27,%28 = %26
in %27
, let %27,%28 = %26
in %28
>
>
in <λ%24...., ...>
in ...
fi
fi
else ...
fi )
...
...
...
...
in ...>
fi in
...
in ...
| inr(%18) =>
...
| inr(%17) =>
...
| inr(%16) =>
...
fi
... in
rec(...)
Definitions occuring in Statement :
q-rel-lub: q-rel-lub(r1;r2),
q-rel-decider: q-rel-decider(r;x),
q-linear: q-linear(k;i.X[i];y),
q_less: q_less(r;s),
qmax-list: qmax-list(L),
qdiv: (r/s),
qpositive: qpositive(r),
qmul: r * s,
qadd: r + s,
qeq: qeq(r;s),
from-upto: [n, m),
l-exists-decider: l-exists-decider(),
l-all-decider: l-all-decider(),
select: L[n],
length: ||as||,
null: null(as),
concat: concat(ll),
filter: filter(P;l),
map: map(f;as),
append: as @ bs,
list_accum: list_accum,
list_ind: list_ind,
tl: tl(l),
hd: hd(l),
cons: [a / b],
nil: [],
genrec-ap: genrec-ap,
bor: p ∨bq,
band: p ∧b q,
primrec: primrec(n;b;c),
evalall: evalall(t),
callbyvalue: callbyvalue,
ifunion: ifunion(b; t),
ifthenelse: if b then t else f fi ,
spreadn: spread4,
spreadn: spread3,
isaxiom: if z = Ax then a otherwise b,
less: if (a) < (b) then c else d,
int_eq: if a=b then c else d,
apply: f a,
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,
subtract: n - m,
add: n + m,
minus: -n,
natural_number: $n,
axiom: Ax
Definitions occuring in definition :
natural_number: $n,
minus: -n,
qmul: r * s,
apply: f a,
qadd: r + s,
lambda: λx.A[x],
pair: <a, b>,
spread: spread def,
map: map(f;as),
subtract: n - m,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spreadn: spread3,
axiom: Ax,
evalall: evalall(t),
select: L[n],
inr: inr x ,
inl: inl x,
qeq: qeq(r;s),
ifthenelse: if b then t else f fi ,
int_eq: if a=b then c else d,
l-exists-decider: l-exists-decider(),
nil: [],
q-rel-decider: q-rel-decider(r;x),
l-all-decider: l-all-decider(),
callbyvalue: callbyvalue,
genrec-ap: genrec-ap,
qdiv: (r/s),
append: as @ bs,
cons: [a / b],
q-linear: q-linear(k;i.X[i];y),
from-upto: [n, m),
less: if (a) < (b) then c else d,
length: ||as||,
filter: filter(P;l),
concat: concat(ll),
q-rel-lub: q-rel-lub(r1;r2),
q_less: q_less(r;s),
qpositive: qpositive(r),
spreadn: spread4,
isaxiom: if z = Ax then a otherwise b,
list_accum: list_accum,
bor: p ∨bq,
hd: hd(l),
tl: tl(l),
list_ind: list_ind,
add: n + m,
primrec: primrec(n;b;c),
null: null(as),
qmax-list: qmax-list(L),
band: p ∧b q,
ifunion: ifunion(b; t)
FDL editor aliases :
q-constraints-decider
Latex:
q-constraints-decider ==
\mlambda{}k.letrec rec(k)=\mlambda{}A.eval z = evalall(A) in
if if k=0 then inl Ax else (inr (\mlambda{}x.Ax) )
then \mlambda{}A.if l-all-decider() A
(\mlambda{}xr.q-rel-decider(let x,y = xr
in y;let x,y = xr in x 0))
then inl []
else inr (\mlambda{}\%6.Ax)
fi
else \mlambda{}A.case l-exists-decider() evalall(A)
(\mlambda{}xr.case if let x,y = xr in y=0 then inl Ax else (inr (\mlambda{}x.Ax) )
of inl(\%2) =>
case if if qeq(let x,y = xr in x k;0)
then inl Ax
else inr (\mlambda{}x.Ax)
fi
then inr (\mlambda{}\%.Ax)
else inl (\mlambda{}\%.Ax)
fi
of inl(\%3) =>
inl <\%2, \%3>
| inr(\%4) =>
inr (\mlambda{}\%.let \%5,\%6 = \%
in Ax)
| inr(\%3) =>
inr (\mlambda{}\%.let \%4,\%5 = \%
in Ax) )
of inl(\%@0) =>
let xr,\%10 = let i,\%1 = \%@0
in <evalall(A)[i], <i, Ax, Ax>, \%1>
in let x1,x2 = xr
in let \%11,\%13,\%14 = \%10 in
case rec (k - 1)
map(\mlambda{}xr.let x,r = xr
in <\mlambda{}j.((x j) + -((x k/x1 k) * (x1 j))), r>
evalall(A))
of inl(\%15) =>
inl (\%15 @ [q-linear(k - 1;j.(-1/x1 k) * (x1 j);\%15)])
| inr(\%16) =>
inr (\mlambda{}\%.Ax)
| inr(\%8) =>
case rec (k - 1)
eval A' = evalall(map(\mlambda{}p.let f,r = p
in eval r = r in
eval as = evalall(map(f;[0, k))) in
<\mlambda{}n.if if (n) < (||as||)
then inl Ax
else (inr Ax )
then as[n]
else f n
fi
, r
>
filter(\mlambda{}a.qeq(let x,y = a in x k;0);
evalall(A))
@ concat(map(\mlambda{}a.map(\mlambda{}b.<\mlambda{}j.(((let x,y = a
in x
k)
* (let x,y = b
in x
j))
+ -((let x,y =
b
in x
k)
* (let x,y =
a
in x
j)))
, ...
>
filter(\mlambda{}c.q\_less(...
k;0);
evalall(A)));
filter(\mlambda{}b.q\_less(0;let x,y =
b
in x
k);
evalall(A)))))) in
A'
of inl(\%) =>
inl case l-exists-decider() evalall(A)
(\mlambda{}a.if qpositive((let x,y = a in x k) + -(0))
then inl Ax
else inr (\mlambda{}x.Ax)
fi )
of inl(\%@0) =>
case l-exists-decider() evalall(A)
(\mlambda{}a.if qpositive(0 + -(let x,y = a in x k))
then inl Ax
else inr (\mlambda{}x.Ax)
fi )
of inl(\%17) =>
let b,\%28,\%30,\%31 =
let a,\%25,\%26 = if if if map(\mlambda{}c.(-((1/let x,y = c in x k))
* q-linear(k - 1;j.let x,y = c
in x
j;\%));
filter(\mlambda{}c.q\_less(let x,y = c
in x
k;0);
evalall(A))) = Ax then inl Ax
otherwise inr Ax
then inl Ax
else inr Ax
fi
then ɘ, Ax, \mlambda{}i.Ax>
else let u,v = map(\mlambda{}c.(-((1/let x,y = c in x k))
* q-linear(k - 1;j.let x,y = c in x j;\%));
filter(\mlambda{}c.q\_less(let x,y = c in x k;0);
evalall(A)))
in <accumulate (with value x and list item y):
if eval r' = evalall(x) in
eval s' = evalall(y) in
qpositive(s' + -(r')) \mvee{}\msubb{}qeq(r';s')
then x
else y
fi
over list:
tl([u / v])
with starting value:
hd([u / v]))
, if if if [u / v] = Ax then inl Ax otherwise inr Ax
then inl Ax
else inr Ax
fi
then Ax
else let u,v = [u / v]
in rec-case(v) of
[] => \mlambda{}-any.ɘ, Ax, Ax>
a::L =>
r.\mlambda{}u@0.if if eval r' = evalall(u@0) in
eval s' = evalall(a) in
qpositive(s' + -(r')) \mvee{}\msubb{}qeq(r';s')
then inl Ax
if if eval r' = evalall(u@0) in
eval s' = evalall(a) in
qpositive(s' + -(r'))
\mvee{}\msubb{}qeq(r';s')
then inl Ax
else inr Ax
fi
then Ax
else inr Ax
fi
then case case case let i,\%2,\%3 = r
u@0 in
if case if i=0
then inl Ax
else (inr Ax )
of inl(x) =>
inl x
| inr(x) =>
inr (\mlambda{}x.Ax)
then \mlambda{}\%,\%4. (inl Ax)
else \mlambda{}\%,\%6. (inr <i
- 1
, Ax
, Ax>\000C )
fi
Ax
Ax
of inl(\%9) =>
inl Ax
| inr(\%10) =>
inr inr \%10
of inl(-any) =>
inl Ax
| inr(-any) =>
inr case -any
of inl(\%1) =>
ɘ, Ax, Ax>
| inr(\%2) =>
let i,\%4,\%5 = \%2 in
<i + 1, Ax, Ax>
of inl(\%1) =>
ɘ, Ax, Ax>
| inr(\%2) =>
let i,\%4,\%5 = \%2 in
<i + 1, Ax, Ax>
else let i,\%4,\%5 = r a in
<i + 1, Ax, Ax>
fi
u
fi
, let \%7,\%8 =
primrec(||[u / v]|| + 1;\mlambda{}n.Ax;
\mlambda{}i,x,n. if if n=(i + 1) - 1
then inl Ax
else (inr (\mlambda{}x.Ax) )
then \mlambda{}L,\%7,a. if if if L = Ax
then inl Ax
otherwise inr Ax
then inl Ax
else inr Ax
fi
then Ax
else let u,v = L
in if null(v)
then <\mlambda{}-any,i. -any
, \mlambda{}-any.(-any
0)
>
else let \%18,\%19 =
let \%23,\%24 =
...
in <\mlambda{}\%24....
, ...
>
in <\mlambda{}-any....
, \mlambda{}-any....
>
fi
fi
else x n
fi )
||[u / v]||
[u / v]
case case if if (||[u / v]||) < (||[u / v]||)
then inl Ax
else (inr (\mlambda{}x.Ax) )
then inr (\mlambda{}\%.Ax)
else inl (\mlambda{}\%.Ax)
fi
of inl(\%2) =>
inl <\%2, Ax, Ax>
| inr(\%3) =>
inr (\mlambda{}\%.let \%4,\%5 = \%
in Ax)
of inl(\%3) =>
\%3
| inr(\%4) =>
Ax
accumulate (with value x and list item y):
if eval r' = evalall(x) in
eval s' = evalall(y) in
qpositive(s' + -(r')) \mvee{}\msubb{}qeq(r';s')
then ...
else ...
fi
over list:
...
with starting value:
...)
in ...>
fi in
...
in ...
| inr(\%18) =>
...
| inr(\%17) =>
...
| inr(\%16) =>
...
fi
... in
rec(...)
Date html generated:
2020_05_20-AM-09_30_34
Last ObjectModification:
2020_01_08-PM-10_01_08
Theory : rationals
Home
Index