-------------------------------------------------------- ALLIGATOR 1.0 MANUAL Paul Piwek Centre for Research in Computing The Open University, UK April, 2006; Updated May 3, 2006 -------------------------------------------------------- Contents -------- - License - Documentation URL - Abstract - Main Predicate - Parameters - Running Alligator and Examples of queries - Exception Handling License ------- ALLIGATOR is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 2.0 England & Wales License. To view a copy of this licence, visit http://creativecommons.org/licenses/by-nc-sa/2.0/uk/ or send a letter to Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA. Documentation ------------- Further documentation on ALLIGATOR is available at http://mcs.open.ac.uk/pp2464/alligator Abstract -------- ALLIGATOR is an experimental prototype of a theorem prover for Pure Type Systems extended with Sigma Types. It also deals with a restricted form of definitions. It has been implemented in Sicstus Prolog and been tested with version 3.12.2 of Sicstus. There is also a version of ALLIGATOR available for (the freely available) SWI Prolog (http://www.swi-prolog.org/). Main Predicate -------------- The main predicate is: prove(+Pseudo_Context,-Term:+Goal) Term is a Prolog variable which the system will instantiate with a proof term for Goal, if such a term exists (given a certain maximum search depth and search time, see below). Otherwise, the call fails. Formally, Goal is a pseudo term. Pseudo-terms (PT) are defined as follows: PT ::= S | V | A | PT-PT | pair(PT,PT) | pi1(PT) | pi2(PT) | lambda(V:PT,PT) | pi(V:PT,PT) | sigma(V:PT,PT) V ::= Prolog Variable A ::= Prolog Atom S ::= type_prop | type_set | prop | set The constructors -, pair(x,y), pi1, pi2, lambda, pi and sigma stand, respectively, for function application (left associative), pairs (i.e., (x,y)), left and right projection, lambda abstraction, (dependent) function types and (dependent) product types. In order to facilitate manual input of pseudo terms we allow for the following abbreviations: Shorthand Notation: [V1:PT1,..,Vn:PTn]=>PT = pi(V1:PT1,..(pi(Vn:PTn,PT)..) [V1:PT1,..,Vn:PTn]/\PT = sigma(V1:PT1,..(sigma(Vn:PTn,PT)..) PT -> PT = pi(V1:PT1,PT), provided V1 does not occur in PT. PT & PT = sigma(V1:PT1,PT), provided V1 does not occur in PT. ~ PT = pi(V1:PT,false) PT1\/PT2 = pi(V1:(pi(V2:A,false)),PT2) Pseudo contexts are Prolog lists containing introductions which are of the form A:PT or def(A,PT1):PT2. Here, A is a Prolog atom. In general, we represent bound PTS variables (bound by lambda, pi or sigma) with Prolog variables. All other PTS variables (unbound) are represented using Prolog atoms. This allows us to use the build-in Prolog unification for comparing pseudo-terms. Parameters ---------- Before the user calls the predicate prove, it is possible to set a number of parameters, using setval(+Param,+Value). The parameters and respective values in question are: 1. feedback with values on/off: for error report and status reports of the proof process (search depth); 2. base_context with values classic/falsum/...: for setting the base contexts that should be loaded. classic consists of dn_pr:([P:prop]=>(((P->false)->false)->P)) and falsum consists of false:prop; 3. maxtime with number of seconds as value: maximum time that the proof search should continue; 4. maxdepth with integer as value: maximum search depth at which the system should search for a proof. The proof search always proceeds using the consecutive-bounded depth-first strategy; 5. startdepth with integer as value: the depth at which the consecutive-bounded depth-first strategy starts searching for proofs. Finally, there are two parameters for determining how long reduction should continue and what proportion of memory reduction is allowed to use (to avoid looping and memory overflow for terms that do not normalize: 6. reduce_time_out with value in milliseconds 7. reduce_space_out with value a number in [0..1] When alligator is consulted or compiled, the default settings of all the aforementioned parameters are printed to the screen (default values can be modified by changing the corresponding val(Param,Val) clauses in the source code): - feedback on; - maximum search time: 3600 seconds; - start search depth: 1; - maximum search depth: 50; - maximum time for reduce: 2500 milliseconds; - maximal proportion of global stack for reduce: 0.9. ALLIGATOR implements Pure Type Systems. Pure Type Systems are highly flexible in terms of the dependent type systems that can be implemented in them. The following clauses in the source code specificy the system that ALLIGATOR uses by default (it can be modified manually in the source code): %%% TYPE SYSTEM: LambdaPREDomega extended with Sigma Types % The type system that we use here is LambdaPREDomega % which can be used for higher order predicate logic. % Sigma's can be added without losing consistency % for Sigma(X:A:,B) with A:Set. %%% SORTS sorts([set,type_set,prop,type_prop]). %%% AXIOMS axioms([(set,type_set), (prop,type_prop)]). %%% TYPE SYSTEM RULES pi_rules([ (set,set), (set,type_prop), % Can be used to make A->prop % and A->(A->prop). % The domains of unary preds and % binary relations. (type_prop,type_prop), % (A->prop)->prop:type_prop; % ((A->prop)->prop->)prop:type_prop % Quantification over type_prop % covering % all higher order domains. (prop,prop), % For forming implications. (set,prop), % For universal quantification over % set types. (type_prop,prop)]). % Quantification over domains of type % type_prop such % as A->prop and A->(A->prop). sigma_rules([(set,prop), % Existential quantification over set % types. (prop,prop)]). % Conjunction. % Note that we cannot have the lambda % cube's (box,star) % which is here (type_set/type_prop, % set/prop). % Addition of the latter rules makes % the system lose % strong normalization and consequently % consistency (see Geuvers, 1994). Running Alligator and Examples of queries ----------------------------------------- To run ALLIGATOR follow these steps: 1. Start Sicstus Prolog. 2. Compile or consult the file alligator1.0.pl. 3. The following message will appear: Alligator 1.0, January 2006. Author: Paul Piwek. - feedback on; - maximum search time: 3600 seconds; - start search depth: 1; - maximum search depth: 50; - maximum time for reduce: 2500 milliseconds; - maximal proportion of global stack for reduce: 0.9. 4. Type your query for alligator (or change the values of parameters using setval as described above). EXAMPLE 1: In the following example we have two sets, a and b and an inhabitant x of a. There is also a function f from set a to set b. In this context we ask for an inhabitant of set b. | ?- prove([a:set,b:set,f:a->b,x:a],X:b). ...context normalized to standard notation and reduced. ...checked context. ...context normalized to arrow notation. ...forward inferences completed. The following Context will be used to construct a proof: false:prop a:set b:set f:[_160:a]=>b x:a dn_pr:[_586:prop,_590:[_598:[_606:_586]=>false]=>false]=>_586 ...searching at depth: 1 2 ...proof found after 0.030 seconds. ...the goal in input notation: b ...the goal in arrow notation: b ...the reduced goal in standard notation: b ...the unreduced proof with atoms and arrows: f-x ...the unreduced proof: f-x ...the reduced proof: f-x ...type checking of the proof succeeded ...the type of b is set X = f-x ? EXAMPLE 2: p or q implies that it is not the case that not p and not q. | ?- prove([p:prop,q:prop],_E: ( p \/ q) -> ~ ( ~ p & ~q)). ...context normalized to standard notation and reduced. ...checked context. ...context normalized to arrow notation. ...forward inferences completed. The following Context will be used to construct a proof: false:prop p:prop q:prop dn_pr:[_729:prop,_733:[_741:[_749:_729]=>false]=>false]=>_729 ...searching at depth: 1 2 3 4 5 ...proof found after 0.030 seconds. ...the goal in input notation: p\/q-> ~ (~p& ~q) ...the goal in arrow notation: [_272:[_278:[_284:p]=>false]=>q]=>[_251:sigma (_263:[_269:p]=>false,[_260:q]=>false)]=>false ...the reduced goal in standard notation: pi(_272:pi(_278:pi(_284:p,false),q), pi(_251:sigma(_263:pi(_269:p,false),pi(_260:q,false)),false)) ...the unreduced proof with atoms and arrows: lambda(v_42:[_2522:[_2530:p]=> false]=>q,lambda(v_43:sigma(_2688:[_2696:p]=>false,[_2685:q]=>false),def (v_44,pi2(v_43))-(v_42-def(v_45,pi1(v_43))))) ...the unreduced proof: lambda(_5699:pi(_2522:pi(_2530:p,false),q),lambda(_5722: sigma(_2688:pi(_2696:p,false),pi(_2685:q,false)),def(v_44,pi2(_5722))-(_5699-def (v_45,pi1(_5722))))) ...the reduced proof: lambda(_583:pi(_623:pi(_629:p,false),q),lambda(_589:sigma (_608:pi(_614:p,false),pi(_605:q,false)),pi2(_589)-(_583-pi1(_589)))) ...type checking of the proof succeeded ...the type of pi(_1330:pi(_1364:pi(_1370:p,false),q),pi(_1525:sigma (_1541:pi(_1547:p,false),pi(_1538:q,false)),false)) is prop yes EXAMPLE 3: b is a set, a is an inhabitant of b and c is predicate over set b. f is a proof that every b has the property c. The goal is to prove that there is a b which is a c. | ?- prove([b:set,a:b,c:[X:b]=>prop,f:pi(X:b,c-X)],_A:[S:b]/\c-S). ...context normalized to standard notation and reduced. ...checked context. ...context normalized to arrow notation. ...forward inferences completed. The following Context will be used to construct a proof: false:prop b:set a:b c:[_217:b]=>prop f:[_200:b]=>c-_200 dn_pr:[_676:prop,_680:[_688:[_696:_676]=>false]=>false]=>_676 ...searching at depth: 1 2 3 ...proof found after 0.030 seconds. ...the goal in input notation: [_43:b]/\c-_43 ...the goal in arrow notation: sigma(_306:b,c-_306) ...the reduced goal in standard notation: sigma(_306:b,c-_306) ...the unreduced proof with atoms and arrows: pair(a,f-a) ...the unreduced proof: pair(a,f-a) ...the reduced proof: pair(a,f-a) ...type checking of the proof succeeded ...the type of sigma(_798:b,c-_798) is prop true ? Exception Handling ------------------ Malformed input (terms, contexts) are handled as exceptions. We use the predicate throw/1 to report such exceptions (see SWI or Sicstus manual; they can be caught with catch/3). We have the following exceptions (note that in verbose mode feedback also writes a brief description of the exception to the screen): error_variable_not_fresh error_cyclic_type error_has_no_type error_unbound_variable error_context_not_existing error_syntax_var_incorrect error_synt_incorrect_var_in_context error_reduction_failed([TimeOut,SpaceOut,Cyclic,FreeVars,SafeTerm]) with TimeOut :== time_out | success with SpaceOut :== space_out | success with Cyclic :== cyclic | not_cyclic with FreeVars :== free_vars | no_free_vars with SafeTerm :== safe | not_safe