--------------------------------------------------------
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