ALLIGATOR Examples ------------------ Tested April 2006 Updated May 3 2006 Table of Contents ----------------- 1. REDUCTION 2. PROVE 3. MISCELLANEOUS 1. REDUCTION ------------ | ?- reduce(lambda(X:a,f-(lambda(Y:a,f-Y-Y)-b)-X-X)-d,R,F). F = [success,success,not_cyclic,no_free_vars,safe], R = f-(f-b-b)-d-d ? yes | ?- reduce(lambda(X:a,lambda(Y:b,f-Y)-X)-c,R,F). F = [success,success,not_cyclic,no_free_vars,safe], R = f-c ? yes | ?- reduce(lambda(X:a,X-f)-lambda(Y:b,g-Y),R,F). F = [success,success,not_cyclic,no_free_vars,safe], R = g-f ? yes | ?- reduce(lambda(X:a,X-f)-lambda(Y:b,lambda(Z:c,Z-f)-Y),R,F). F = [success,success,not_cyclic,no_free_vars,safe], R = f-f ? yes | ?- reduce(lambda(P:pred,P-john)-lambda(X:person,walk-X),R,F). F = [success,success,not_cyclic,no_free_vars,safe], R = walk-john ? yes | ?- reduce(lambda(B:a,(z-(B-c)))-lambda(X:d,lambda(Y:q,X-Y)-p),R,F). F = [success,success,not_cyclic,no_free_vars,safe], R = z-(c-p) ? yes | ?- reduce(lambda(X:a,X-a-(X-b))-lambda(Y:b,Y),R,F). F = [success,not_cyclic,no_free_vars,safe], R = a-b ? yes | ?- reduce(lambda(Y:a,Y-Y-Y)-lambda(X:a,X-X),R,Z). Z = [success,space_out,not_cyclic,no_free_vars,safe] ? yes | ?- reduce(lambda(Y:a,Y-A-Y)-lambda(X:a,X-X),R,Z). Z = [_A,_B,_C,free_vars,_D] ? yes | ?- reduce(lambda(X:a,X)-lambda(X:a,X-X),R,Z). Z = [_A,_B,_C,_D,not_safe] ? yes | ?- reduce_term(lambda(X:a,X)-lambda(X:a,X-X),R). ERROR: Reduction of term lambda(_455:a,_455)-lambda(_455:a,_455-_455) failed. ! error_reduction_failed([_63,_61,_59,_57,not_safe]) | ?- reduce(lambda(Y:a,Y-Y)-lambda(X:a,X-X),R,Z). Z = [success,space_out,not_cyclic,no_free_vars,safe] ? yes | ?- reduce_term(lambda(Y:a,Y-Y)-lambda(X:a,X-X),R), print(R). ERROR: Reduction of term lambda(_41:a,_41-_41)-lambda(_42:a,_42-_42) failed. ! error_reduction_failed 2. PROVE -------- OK | ? - prove([a:prop,x:a],X:a). X = x ? ; X = dn_pr-a-lambda(_A:pi(_B:a,false),_A-x) ? ; OK | ? - prove([b:prop,a:prop,x:a,f:pi(X:a,b)],_Y:b). OK | ? - prove([a:set,x:a,b:pi(Z:a,prop),f:pi(X:a,b-X)],_Y:b-x). % This one returns no because b hasn't been introduced: NO | ? - prove([p:sigma(X:a,b)],_Y:b). OK | ? - prove([a:set,b:prop,p:sigma(X:a,b)],_Y:b). OK | ?- prove([a:set,b:prop,c:prop,f:pi(X:b,c),p:sigma(X:a,b)],_Y:c). For all X: X -> X: OK |? - prove([],_Z:pi(X:prop,pi(Y:X,X))). For all P:prop, Q:prop: P->(Q->P) OK |? - prove([],_Z:pi(P:prop,pi(Q:prop,pi(X:P,pi(Y:Q,P))))). % This is contraposition if b is the false/contradiction: OK |? - prove([b:prop],_Z:pi(P:prop,pi(Q:prop,pi(X:pi(Y:P,Q),pi(Z:pi(A:Q,b),pi(B:P,b)))))). % This is contraposition if b is the false/contradiction: OK |? - prove([b:prop],_CP:[P:prop,Q:prop,G1:([X:P]=>Q),G2:([Y:Q]=>b)]=>([Z:P]=>b)). OK |? - prove([b:prop,p:prop,q:prop,u:prop,c:[Y:[E:[X:p]=>b]/\[Z:q]=>b]=>b,bh:[X:q]=>u,ah:[X:p]=>u,dn:([P:prop,Q:([R:([S:P]=>b)]=>b)])=>P],_Z:u). % The following one fails, because we do not have sigma types for % (set,set). Note that the program gets into a backtracking loop. NO |? - prove([a:set,b:set,x:a,f:pi(Z:a,b)],_A:sigma(X:a,b)). OK | ?- prove([e:set,a:e,b:e,c:e,r:([V:e,W:e]=>prop), f:[X:e,Y:e,Z:e,P1:r-X-Y,P2:r-Y-Z]=>r-X-Z, p3:r-a-c,p4:r-c-b],ZZ:r-a-b). OK |? - prove([e:set,a:e,b:e,c:e,r:[V:e,W:e]=>prop,f:[X:e]=>r-X-X],_P:[Z:e,E:e]/\r-Z-E). % Exist x All y |- All y Exist x OK | ?- prove([e:set,r:[P:e,Q:e]=>prop,f:[X:e]/\([Y:e]=>r-X-Y)],_G:[Y1:e]=>([X1:e]/\r-X1-Y1)). % |- p->q or q->p OK | ?- prove([b:prop,p:prop,q:prop,dn:([P:prop,Q:([R:([S:P]=>b)]=>b)])=>P],_G: [Z:[Y:[X:p]=>q]=>b]=>[W:q]=>p). % (p or q) -> r |- (p -> r) % ((p -> b) -> q) -> r | p -> r % (We need double negation) OK | ?- prove([b:prop,p:prop,q:prop,r:prop,dn:([P:prop,Q:([R:([S:P]=>b)]=>b)])=>P],_G: [H:[Z:[Y:[X:p]=>b]=>q]=>r]=>[M:p]=>r). % Use the classic context OK | ?- prove([p:set,q:prop],_P:p->q->((q->false)->(p->false))). % This one requires the rule for false and dn OK | ?- prove([p:prop],_X:(p\/ ~p)->(~p \/ p)). OK | ?- prove([p:prop,q:prop],_P:p->(q->p)). % For this one type checking takes rather long (note that proof construction is fast, within 0.241 seconds in Sicstus; SWI seems to take longer): OK | ?- prove([p:prop,q:prop,r:prop,s:prop,t:prop,u:prop,v:prop,z:prop],_P:((p \/ q \/ r \/ s \/ t \/ u \/ v) -> z) -> (p -> z)). OK | ?- prove([p:prop,q:prop,r:prop,s:prop,t:prop,u:prop,v:prop,z:prop],_P:((p \/ q \/ r) -> z) -> (p -> z)). OK | ?- prove([p:prop,q:prop,r:prop],_X:(p->(q->r))->((p->q)->(p->r))). OK prove([a:prop,b:prop],_G:sigma(X:a,b)->sigma(Y:b,a)). OK | ?- prove([],_X:[P:prop,Q:prop,R:prop]=>(P->(Q->R))->((P->Q)->(P->R))). OK | ?- prove([p:prop,q:prop],_X:(p->(q->(p->q)))->((p->q)->(p->(p->q)))). % ERROR: the variable false is not fresh (already defined in the base_context) NO | ?- prove([a:(~p)->(~q),b:q,p:prop,q:prop,f:[P:prop,Q:false]=>P,false:prop],_X:p). % Ax Ey Rxy -> Ax Rxx (Not valid!) NO | ?- prove([e:set,r:[X:e,Y:e]=>prop,a1:[X:e]=>([Y:e]/\r-Y-X)],_Z:[X:e]=>r-X-X). % Ax Rxx -> Ax Ey Rxy OK | ?- prove([e:set,r:[X:e,Y:e]=>prop,a1:[X:e]=>r-X-X],_Q:[X:e]=>([Y:e]/\r-Y-X)). OK prove([p:prop],_R: ~ (~p) -> p). OK prove([p:prop,q:prop,a1: ~ ~p,a2:p->q],_R:q). OK prove([p:prop,q:prop,u:prop,a1: ~ ( ~p -> ~q),a2:q->u],_R:u). OK prove([p:prop,g:prop,x:prop,a1:g->p,a2: ~ x -> ~ p],_R:g->x). OK | ?- prove([p:prop,g:prop,x:prop,a1:g->p,a2: ~ ~ (~ x -> ~ p)],_R:g->x). OK prove([p:prop,q:prop],_R:(p->q)\/(q->p)). NO prove([p:prop,q:prop],_R:p). OK prove([e:set,p:prop,q:prop,r:e->prop,f:e->e,g:[X:e]=>(r-X)->r-(f-X),a1:e,a2:r-a1],_R:r-(f-(f-a1))). OK prove([a:prop,b:prop,c:prop],_B:(a&b)->(a\/b)). OK prove([a:prop,b:prop,c:prop],_B:(a&(b\/c))->(a&b)\/(a&c)). OK prove([p:prop,q:prop],_E: ~ ( ~p & ~q) -> p\/q). OK prove([p:prop,q:prop],_E: ( p \/ q) -> ~ ( ~ p & ~q)). % should not work: NO prove([e:set, p:e->prop],_E: ([X:e]=> ~ p-X) -> sigma(Y:e,p-Y)) prove([e:set, p:e->prop],_E: ([X:e]=> ~ p-X) -> ~ sigma(Y:e,p-Y)). % Not for all X p-X entails that there is an Y not p-Y * OK prove([e:set, p:e->prop],_E: ~ ([X:e]=> p-X) -> sigma(Y:e, ~ p-Y)). OK prove([e:set, p:e->prop,a1: ~ ([X:e]=> p-X), a2: ~ sigma(Y:e,~ p-Y)],_E:false). % Not valid For all X Exist Y m-X-Y entails Exist Z For all T m-T-Z: * no proof: prove([e:set, m:e->(e->prop),a1:([X:e]=> sigma(Y:e,m-X-Y))],_E:sigma(Z:e,[T:e]=>m-T-Z)). * prove([e:set, m:e->(e->prop),a1:sigma(X1:e,[X2:e]=>m-X1-X2)],_E:([Y1:e]=> sigma(Y2:e,m-Y2-Y1))). OK prove([p:prop,r:prop,q:((p->false)->r),z:r->false],_E:p). OK prove([p:prop,q:prop,a1:(((sigma(X:p,q))->false)->false)],_E:sigma(Y:p,q)). OK prove([e:set,a:e,pred:(e->prop),p:pred-a],_X:sigma(X:e,pred-X)). OK prove([a:prop,b:prop],_G:a \/ (~ b) -> ((~ b) \/ a)). OK prove([a:prop,b:prop,c:prop],_G:(a & (b \/ c)) -> ((a&b) \/ (a&c))). OK prove([a:prop,b:prop],_G:a \/ b -> b \/ a). OK prove([a:prop,b:prop,c:prop],_G:(a&c) \/ b -> b \/ (c&a)). OK prove([e:set,r:e->prop,p1:sigma(Y:e,r-Y)],P:sigma(X:e,r-X)). OK prove([e:set,r:e->prop,p1: ~ ~ sigma(Y:e,r-Y)],P:sigma(X:e,r-X)). OK prove([e:set,r:e->prop,s:e->prop,p1:sigma(Y:e,r-Y),p2:[Z:e,Q:r-Z]=>s-Z],P:sigma(X:e,s-X)). OK prove([e:set,r:e->prop,s:e->prop,t:e->prop,p1:sigma(Y:e,r-Y),p2:[Z:e,Q:r-Z]=>s-Z,p3:[A:e,B:s-A]=>t-A],P:sigma(X:e,t-X)). OK prove([e:set,r:e->prop,s:e->prop,t:e->prop,p1: ~ ~ sigma(Y:e,r-Y),p2:[Z:e,Q:r-Z]=>s-Z,p3:[A:e,B:s-A]=>t-A],P:sigma(X:e,t-X)). OK prove([e:set,r:e->prop,s:e->prop,t:e->prop,p1:sigma(Y:e,r-Y),p2: ~ ~ ([Z:e,Q:r-Z]=>s-Z),p3:[A:e,B:s-A]=>t-A],P:sigma(X:e,t-X)). NO prove([thing:set,v:thing->prop,p:thing->prop,q:thing->prop,f1:([X1:thing,F1:p-X1]=>v-X1),f2:([X2:thing,F2:q-X2]=>v-X2),p1:( ~ sigma(X:thing,p-X))->sigma(Y:thing,q-Y)],_X:sigma(Z:thing,v-Z)) OK prove([thing:set,v:thing->prop,p:thing->prop,q:thing->prop,f1:([X1:thing,F1:p-X1]=>v-X1),f2:([X2:thing,F2:q-X2]=>v-X2),p1:sigma(Y:thing,q-Y)],_X:sigma(Z:thing,v-Z)) OK prove([thing:set,v:thing->prop,p:thing->prop,q:thing->prop,f1:([X1:thing,F1:p-X1]=>v-X1),f2:([X2:thing,F2:q-X2]=>v-X2),p1: ~ ~ sigma(Y:thing,q-Y)],_X:sigma(Z:thing,v-Z)) NO prove([a:prop,thing:set,v:thing->prop,p:thing->prop,q:thing->prop,f1:([X1:thing,F1:p-X1]=>a),f2:([X2:thing,F2:q-X2]=>a),p1: ~ sigma(Y:thing,q-Y) -> sigma(Q:thing,p-Q)],_X:a) OK prove([a:prop,thing:set,v:prop,p:prop,q:prop,f1:([X1:thing,F1:p]=>a),f2:([X2:thing,F2:q]=>a),p1: ~ sigma(Y:thing,q) -> sigma(Q:thing,p)],_X:a) OK prove([thing:set,a:thing->prop,v:prop,p:prop,q:prop,f1:([X1:thing,F1:p]=>a-X1),f2:([X2:thing,F2:q]=>a-X2),p1: ~ sigma(Y:thing,q) -> sigma(Q:thing,p)],_X:sigma(Z:thing,a-Z)) OK prove([b:prop,p:prop,q:prop,u:prop,a3:[X:p->false]=>q,a1:p->u,a2:q->u],_Z:u). OK prove([e:set,q:e->prop,a1:(((sigma(X:e,q-X))->false)->false)],_E:sigma(Y:e,q-Y)). OK prove([v:prop,p:prop,q:prop,f1:p->v,f2:q->v,thing:set,p1:(sigma(X:thing,p)->false)->sigma(Y:thing,q)],_X:sigma(Z:thing,v)) 3. MISCELLANEOUS ---------------- OK | ? - initialize_fresh_vars([a:g,bb:c],[e,w]). OK | ?- standard_notat(([P1:set,Q1:([R1:([S1:P1]=>b)]=>b)])=>P1,NN). NN = pi(P1:set,pi(Q1:pi(R1:pi(S1:P1,b),b),P1)) ? yes OK | ?- standard_context_notat([e:set,a:e,b:e,c:e,r:([V:e,W:e]=>prop),f:([X:e,Y:e,Z:e,P1:r-X-Y,P2:r-Y-Z]=>r-X-Z),p3:r-a-c,p4:r-c-b],R),arrow_context_notat(R,FF),forward_context(FF,Z). R = [e:set,a:e,b:e,c:e,r:pi(_A:e,pi(_B:e,prop)),f:pi(_C:e,pi(_D:e,pi(_E:e,pi(...)))),p3:r-a-c,p4:r-c-b], Z = [r:[_H:e,_I:e]=>prop,f:[_J:e,_K:e,_L:e,_M:r-_J-_K,_N:r-_K-_L]=>r-_J-_L,e:set,a:e,b:e,c:e,p3:r-a-c,p4:r-c-b], FF = [e:set,a:e,b:e,c:e,r:[_O:e]=>[_P:e]=>prop,f:[_Q:e]=>[_R:e]=>[_S:e]=>[_T:r-_Q-_R]=>[_U:r-_R-_S]=>r-_Q-_S,p3:r-a-c,p4:r-c-b] ? yes OK check_type2(lambda(X:a,b),Y,[a:set,b:a]). OK check_type(sigma(Y:e,sigma(X:q,p)),R,[q:prop,p:prop,e:set]) % should not work: NO check_type2(lambda(_911:lambda(_926:a,_926),lambda(_913:pi(_919:a,false),pi2(_911))),T,[a:prop,false:prop]). OK check_type2(lambda(_963:sigma(_980:a,b),lambda(_965:pi(_971:a,false),pi2(_963))),R,[a:prop,b:prop,false:prop]). OK | ?- standard_context_notat([e:set,r:[X:e,Y:e]=>prop,a1:[X:e]=>r-X-X],R),check_type(lambda(_9853:e,pair(_9853,a1-_9853)),B,R). B = pi(_A:e,sigma(_B:e,r-_B-_B)), R = [e:set,r:pi(_C:e,pi(_D:e,prop)),a1:pi(_E:e,r-_E-_E)] ? yes OK | ?- check_type2(lambda(_1539:sigma(_1587:a,pi(_1578:pi(_1584:b,false),c)),lambda(_1530:pi(_1560:sigma(_1566:a,b),false),pair(pi1(_1539),pi2(_1539)-lambda(_1534:b,_1530-pair(pi1(_1539),_1534))))),R,[a:prop,b:prop,c:prop,false:prop]). R = pi(_1539:sigma(_1587:a,pi(_1578:pi(_1584:b,false),c)),pi(_A:pi(_B:sigma(_C:a,b),false),sigma(_D:a,c))) ? yes