Commit 84e29d99 authored by Raphael Cauderlier's avatar Raphael Cauderlier

arity -> domain

parent 8b720c66
......@@ -25,9 +25,9 @@ def 2 := nat.S 1.
(; Signature ;)
A : sort.
LEQ : predicate.
[] fol.pred_arity LEQ --> read_sorts 2 A A.
[] fol.pred_domain LEQ --> read_sorts 2 A A.
N : function.
[] fol.fun_arity N --> nil_sort.
[] fol.fun_domain N --> nil_sort.
[] fol.fun_codomain N --> A.
def leq : term A -> term A -> prop := pred_apply LEQ.
......
......@@ -12,13 +12,13 @@ BAR : fol.sort.
(; We have to assume that the bar is not empty, that is we have a term
of sort BAR. Let's call it Joe. ;)
JOE : fol.function.
[] fol.fun_arity JOE --> fol.nil_sort.
[] fol.fun_domain JOE --> fol.nil_sort.
[] fol.fun_codomain JOE --> BAR.
def Joe : fol.term BAR := fol.fun_apply JOE.
(; The "drink" predicate. ;)
DRINK : fol.predicate.
[] fol.pred_arity DRINK --> fol.read_sorts (nat.S nat.O) BAR.
[] fol.pred_domain DRINK --> fol.read_sorts (nat.S nat.O) BAR.
def drink (x : fol.term BAR) : fol.prop := fol.pred_apply DRINK x.
def drinker_statement : fol.prop :=
......
......@@ -24,12 +24,12 @@ def 1 := nat.S 0.
(; Signature ;)
A : sort.
P : predicate.
[] fol.pred_arity P --> read_sorts 1 A.
[] fol.pred_domain P --> read_sorts 1 A.
O : function.
[] fol.fun_arity O --> nil_sort.
[] fol.fun_domain O --> nil_sort.
[] fol.fun_codomain O --> A.
S : function.
[] fol.fun_arity S --> read_sorts 1 A.
[] fol.fun_domain S --> read_sorts 1 A.
[] fol.fun_codomain S --> A.
def p : term A -> prop := pred_apply P.
......
#NAME clauses.
atom : Type.
mk_atom : p : fol.predicate -> fol.terms (fol.pred_arity p) -> atom.
mk_atom : p : fol.predicate -> fol.terms (fol.pred_domain p) -> atom.
litteral : Type.
pos_lit : atom -> litteral.
......
......@@ -14,12 +14,12 @@ def all := fol.all.
def proof := fol.proof.
def predicate := fol.predicate.
def pred_arity := fol.pred_arity.
def pred_domain := fol.pred_domain.
def pred_apply := fol.pred_apply.
def apply_pred := fol.apply_pred.
def function := fol.function.
def fun_arity := fol.fun_arity.
def fun_domain := fol.fun_domain.
def fun_codomain := fol.fun_codomain.
def apply_fun := fol.apply_fun.
......@@ -28,7 +28,7 @@ def S := nat.S.
(; Equality is a family of binary predicate symbols. ;)
Eq : sort -> predicate.
[A] fol.pred_arity (Eq A) --> read_sorts (S (S O)) A A.
[A] fol.pred_domain (Eq A) --> read_sorts (S (S O)) A A.
def eq (A : sort) : term A -> term A -> prop := pred_apply (Eq A).
[A,x,y]
......@@ -97,8 +97,8 @@ def eq_pred_imp : L : sorts -> p : (terms L -> prop) -> proof (pred_imp L p p).
(H =>
eq_congr A x y H (y : term A => pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => p (cons_term A y L l))) (eq_pred_imp L (l : terms L => p (cons_term A x L l)))))).
thm eq_pred_equal (p : predicate) : proof (pred_imp (pred_arity p) (apply_pred p) (apply_pred p))
:= eq_pred_imp (pred_arity p) (apply_pred p).
thm eq_pred_equal (p : predicate) : proof (pred_imp (pred_domain p) (apply_pred p) (apply_pred p))
:= eq_pred_imp (pred_domain p) (apply_pred p).
def fun_eq : L : sorts -> B : sort -> (terms L -> term B) -> (terms L -> term B) -> prop.
[B,b,b'] fun_eq fol.nil_sort B b b' --> eq B (b nil_term) (b' nil_term)
......@@ -118,5 +118,5 @@ def eq_fun_eq : L : sorts -> B : sort -> f : (terms L -> term B) -> proof (fun_e
(H =>
eq_congr A x y H (y : term A => fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))) (eq_fun_eq L B (l : terms L => f (cons_term A x L l)))))).
thm eq_fun_equal (f : function) : proof (fun_eq (fun_arity f) (fun_codomain f) (apply_fun f) (apply_fun f))
:= eq_fun_eq (fun_arity f) (fun_codomain f) (apply_fun f).
thm eq_fun_equal (f : function) : proof (fun_eq (fun_domain f) (fun_codomain f) (apply_fun f) (apply_fun f))
:= eq_fun_eq (fun_domain f) (fun_codomain f) (apply_fun f).
......@@ -45,10 +45,10 @@ def read_sorts (n : nat) : read_sorts_T n
(; Terms are trees built from function symbols ;)
(; function is the sort of function symbols, ;)
(; each time a function symbol is declared, the functions fun_arity
(; each time a function symbol is declared, the functions fun_domain
and fun_codomain should be extended ;)
function : Type.
def fun_arity : function -> sorts.
def fun_domain : function -> sorts.
def fun_codomain : function -> sort.
(; Function application is unnary ;)
......@@ -59,7 +59,7 @@ cons_term : A : sort -> term A ->
terms tail_types ->
terms (cons_sort A tail_types).
apply_fun : f : function ->
terms (fun_arity f) ->
terms (fun_domain f) ->
term (fun_codomain f).
(; To limit the number of parentheses when writing function
......@@ -75,7 +75,7 @@ def read_f : As : sorts -> C : sort -> (terms As -> term C) -> read_f_T As C.
[C,f] read_f nil_sort C f --> f nil_term.
[A,As,C,f] read_f (cons_sort A As) C f --> a : term A => read_f As C (as : terms As => f (cons_term A a As as)).
def fun_apply (f : function) := read_f (fun_arity f) (fun_codomain f) (apply_fun f).
def fun_apply (f : function) := read_f (fun_domain f) (fun_codomain f) (apply_fun f).
def fun_arrs := read_f_T.
......@@ -84,7 +84,7 @@ def fun_uncurry : As : sorts -> A : sort -> fun_arrs As A -> terms As -> term A.
[A,As,B,f,a,as] fun_uncurry (cons_sort A As) B f (cons_term _ a _ as) --> fun_uncurry As B (f a) as.
def make_fun : As : sorts -> A : sort -> (fun_arrs As A) -> function.
[As] fun_arity (make_fun As _ _) --> As.
[As] fun_domain (make_fun As _ _) --> As.
[A] fun_codomain (make_fun _ A _) --> A.
(; [As, A, f, as] apply_fun (make_fun As A f) as --> fun_uncurry As A f as. ;)
......@@ -191,9 +191,9 @@ def nex (n : nat) : nall_aux2_type nil_sort n := nex_aux2 nil_sort n.
(; Predicate application is also nary ;)
predicate : Type.
def pred_arity : predicate -> sorts.
def pred_domain : predicate -> sorts.
apply_pred : p : predicate ->
terms (pred_arity p) ->
terms (pred_domain p) ->
prop.
(; To limit the number of parentheses when writing predicate
......@@ -210,7 +210,7 @@ def read_p : As : sorts -> (terms As -> prop) -> read_p_T As.
[A,As,p] read_p (cons_sort A As) p -->
a : term A => read_p As (as : terms As => p (cons_term A a As as)).
def pred_apply (p : predicate) := read_p (pred_arity p) (apply_pred p).
def pred_apply (p : predicate) := read_p (pred_domain p) (apply_pred p).
def pred_arrs := read_p_T.
......@@ -219,7 +219,7 @@ def pred_uncurry : As : sorts -> pred_arrs As -> terms As -> prop.
[A,As,p,a,as] pred_uncurry (cons_sort A As) p (cons_term _ a _ as) --> pred_uncurry As (p a) as.
def make_pred : As : sorts -> (pred_arrs As) -> predicate.
[As] pred_arity (make_pred As _) --> As.
[As] pred_domain (make_pred As _) --> As.
(; [As, p, as] apply_pred (make_pred As p) as --> pred_uncurry As p as. ;)
......
......@@ -21,10 +21,10 @@ ONE : fol.function.
ADD : fol.function.
(; Arities ;)
[] fol.pred_arity EQ --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_arity ZERO --> fol.nil_sort.
[] fol.fun_arity ONE --> fol.nil_sort.
[] fol.fun_arity ADD --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.pred_domain EQ --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_domain ZERO --> fol.nil_sort.
[] fol.fun_domain ONE --> fol.nil_sort.
[] fol.fun_domain ADD --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_codomain ZERO --> Nat.
[] fol.fun_codomain ONE --> Nat.
[] fol.fun_codomain ADD --> Nat.
......
......@@ -44,9 +44,8 @@ about [[* Resolution][resolution]].
** Why a multi-sorted logic?
We have chosen to use a multi-sorted version of first-order logic. In
this setting, the arity of a predicate or function symbol is not
simply a natural number but a list of sorts (also known as /types/)
and each function symbol has a codomain sort.
this setting, the domain of a predicate or function symbol is a list
of sorts and each function symbol has a codomain sort.
We use a multi-sorted logic for two reasons. First, some automatic
provers such as Zenon Arith and Zipperposition work in this
......@@ -95,9 +94,9 @@ sort =A= is =fol.term A=; in other words, the Dedukti symbol
A function symbol is a Dedukti term of type =fol.function=.
A codomain and an arity are respectively associated to each function
A domain and a codomain are respectively associated to each function
symbol by the functions
- =fol.fun_arity : fol.function -> fol.sorts= and
- =fol.fun_domain : fol.function -> fol.sorts= and
- =fol.fun_codomain : fol.function -> fol.sort=
If =As= is a list of sorts, then =fol.terms As= is the Dedukti type of
......@@ -108,12 +107,12 @@ lists of terms whose sorts match =As=. This type has two constructors:
The only constructor of =fol.term A= is application of a function
symbol =f= whose codomain is =A= to a list of terms whose sorts match
the arity of =f=.
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_arity f) -> fol.term (fol.fun_codomain f)=
the domain of =f=.
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_domain f) -> fol.term (fol.fun_codomain f)=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a function symbol to terms:
- if =f= is a function symbol of arity =fol.read_sorts n A1 … An= and
- if =f= is a function symbol of domain =fol.read_sorts n A1 … An= and
of codomain =B=, and if =a1=, …, =an= are =n= terms of sort =A1=, …,
=An= respectively, then =fol.fun_apply f a1 … an= has sort =B=.
......@@ -127,20 +126,20 @@ by logical connectives and quantifiers.
**** Atoms
An atom is a predicate symbol applied to terms respecting the arity of
An atom is a predicate symbol applied to terms respecting the domain of
the predicate symbol. Predicate symbols and their arities are defined
similarly to function symbols. A predicate symbol is a Dedukti term of
type =fol.predicate=. An artity is associated to each predicate
symbol by the function
- =fol.pred_arity : fol.predicate -> fol.sorts=
- =fol.pred_domain : fol.predicate -> fol.sorts=
Applying a predicate symbol on a list of terms respecting its arity
Applying a predicate symbol on a list of terms respecting its domain
produces a formula:
- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_arity p) -> fol.prop=
- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_domain p) -> fol.prop=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a predicate symbol to terms:
- if =p= is a predicate symbol of arity =fol.read_sorts n A1 … An= and
- if =p= is a predicate symbol of domain =fol.read_sorts n A1 … An= and
if =a1=, …, =an= are =n= terms of sort =A1=, …, =An= respectively,
then =fol.pred_apply p a1 … an= has type =fol.prop=.
......@@ -221,9 +220,9 @@ corresponding certificates constructors presented in [[* Reasoning][the reasonin
To define a new first-order theory, we start by declaring the sorts,
predicate symbols, and function symbols as new constants of type
=fol.sort=, =fol.predicate=, and =fol.function= respectively. We then
define the arity of each function and predicate symbol and the
define the domain of each function and predicate symbol and the
codomain sort of each function symbol by extending the definitions of
=fol.pred_arity=, =fol.fun_arity=, and =fol.fun_codomain= respectively.
=fol.pred_domain=, =fol.fun_domain=, and =fol.fun_codomain= respectively.
Finally we declare constants for the axioms and axiom schemes of the
theory.
......@@ -244,7 +243,7 @@ We treat equality as a first-order theory defined in the file
a sort:
- =eq.Eq : fol.sort -> fol.predicate=
The predicate symbol =eq.Eq A= expects two terms of sort =A= so the arity of the symbol =eq.Eq A= is =fol.read_sorts (nat.S (nat.S nat.O)) A A=.
The predicate symbol =eq.Eq A= expects two terms of sort =A= so the domain of the symbol =eq.Eq A= is =fol.read_sorts (nat.S (nat.S nat.O)) A A=.
The shortcut notation =eq.eq A a b= where =A= has type =fol.sort= and
both =a= and =b= have type =fol.term A= denotes the formula
......@@ -261,10 +260,10 @@ facts:
=eq.eq_trans : A : fol.sort -> fol.proof (fol.all A (x => fol.all A (y => fol.all A (z => fol.imp (eq.eq A x y) (fol.imp (eq.eq A y z) (eq.eq A x z))))))=
- Equality is a congruence with respect to all function symbols:
=eq.eq_fun_equal : f : fol.function -> fol.proof (fol.all A1 (x1 => fol.all A1 (y1 => fol.imp (eq.eq A1 x1 y1) (… fol.all An (xn => fol.all An (yn => fol.imp (eq.eq An xn yn) (eq.eq B (fol.apply_fun f x1 … xn) (fol.apply_fun f y1 … yn)))) …))))=
where =f= has arity =fol.read_sorts n A1 … An= and codomain =B=.
where =f= has domain =fol.read_sorts n A1 … An= and codomain =B=.
- Equality is a congruence with respect to all predicate symbols:
=eq.eq_pred_equal : p : fol.predicate -> fol.proof (fol.all A1 (x1 => fol.all A1 (y1 => fol.imp (eq.eq A1 x1 y1) (… fol.all An (xn => fol.all An (yn => fol.imp (eq.eq An xn yn) (fol.imp (fol.apply_pred p x1 … xn) (fol.apply_pred p y1 … yn)))) …))))=
where =p= has arity =fol.read_yypes n A1 … An=
where =p= has domain =fol.read_yypes n A1 … An=
* The tactic language
......@@ -494,7 +493,7 @@ can be used for this purpose:
(A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) ->
(A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) ->
(p : fol.predicate ->
fol.terms (fol.pred_arity p) ->
fol.terms (fol.pred_domain p) ->
cert.certificate) ->
cert.certificate
......@@ -519,7 +518,7 @@ on each of the cases:
- =cert.match_imp : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_all : fol.prop -> (A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_ex : fol.prop -> (A : fol.sort -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_pred : fol.prop -> (p : fol.predicate -> fol.terms (fol.pred_arity p) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_pred : fol.prop -> (p : fol.predicate -> fol.terms (fol.pred_domain p) -> cert.certificate) -> cert.certificate -> cert.certificate=
** Sort and formulae comparison
......@@ -620,7 +619,7 @@ reason about equality:
- =eqcert.symmetry : cert.certificate -> cert.certificate=
- =eqcert.transitivity : A : fol.sort -> fol.term A -> cert.certificate -> cert.certificate -> cert.certificate=
- =eqcert.f_equal : f : fol.function -> c1 : cert.certificate -> … -> cn : cert.certificate -> cert.certificate=
(where the arity of =f= has length =n=)
(where the domain of =f= has length =n=)
- =eqcert.rewrite : A : fol.sort -> fol.term A -> fol.term A -> cert.certificate -> cert.certificate=
The certificate =eqcert.match_equality A f c= is equivalent to =f B b1
......
......@@ -215,7 +215,7 @@ def match_prop : prop ->
(A : sort -> (term A -> prop) -> certificate) -> (; all ;)
(A : sort -> (term A -> prop) -> certificate) -> (; ex ;)
(p : fol.predicate ->
fol.terms (fol.pred_arity p) ->
fol.terms (fol.pred_domain p) ->
certificate) ->
certificate.
......@@ -288,7 +288,7 @@ def match_ex (A : prop) (c1 : A : sort -> (term A -> prop) -> certificate) (c2 :
(__ => __ => c2).
def match_pred (A : prop)
(c1 : p : fol.predicate -> fol.terms (fol.pred_arity p) -> certificate)
(c1 : p : fol.predicate -> fol.terms (fol.pred_domain p) -> certificate)
(c2 : certificate) : certificate :=
match_prop A
c2
......
......@@ -86,8 +86,8 @@ def transitivity (A : sort) (b : term A) (c1 : certificate) (c2 : certificate) :
def match_f_equal_goal : prop ->
(f : fol.function ->
fol.terms (fol.fun_arity f) ->
fol.terms (fol.fun_arity f) ->
fol.terms (fol.fun_domain f) ->
fol.terms (fol.fun_domain f) ->
certificate) ->
certificate.
[A,f,as,bs,c] match_f_equal_goal (fol.apply_pred
......@@ -150,10 +150,10 @@ def f_equal_fun_on_goal (L : fol.sorts) (cs : certificates L) : certificate
cert.with_goal (G => match_f_equal_goal G
(f => as => bs =>
f_equal_fun
(fol.fun_arity f)
(fol.fun_domain f)
(fol.fun_codomain f)
(fol.apply_fun f)
as bs (ifeq_certs L (fol.fun_arity f) cs)
as bs (ifeq_certs L (fol.fun_domain f) cs)
)).
def f_equal_T : fol.sorts -> Type.
......@@ -194,7 +194,7 @@ def f_equal_fun_n : L' : fol.sorts ->
def f_equal (f : fol.function) :=
f_equal_fun_n
(fol.fun_arity f)
(fol.fun_domain f)
fol.nil_sort
nil_cert.
......
......@@ -57,7 +57,7 @@ def aproof (a : clauses.atom) := proof (aprop a).
def unify_atoms_pb : clauses.atom -> clauses.atom -> unif.unify_problem.
[p,l,l'] unify_atoms_pb (clauses.mk_atom p l) (clauses.mk_atom p l') -->
unif.unify_cons_terms (fol.pred_arity p) l l' unif.unify_nil.
unif.unify_cons_terms (fol.pred_domain p) l l' unif.unify_nil.
def unify_atoms (a : clauses.atom) (a' : clauses.atom) : subst :=
get_subst (unif.unify' (unify_atoms_pb a a')).
......
......@@ -24,10 +24,10 @@ def imp := fol.imp.
def all := fol.all.
def ex := fol.ex.
def apply_pred := fol.apply_pred.
def pred_arity := fol.pred_arity.
def pred_domain := fol.pred_domain.
def apply_fun := fol.apply_fun.
def fun_apply := fol.fun_apply.
def fun_arity := fol.fun_arity.
def fun_domain := fol.fun_domain.
def function := fol.function.
def read_sorts := fol.read_sorts.
def proof := fol.proof.
......@@ -53,14 +53,14 @@ def subst_proof_rev : s : substitution -> A : prop -> proof (subst_prop s A) ->
[s,A,p] subst_prop s (fol.all A p) --> all A (x : term A => subst_prop s (p x))
[s,A,p] subst_prop s (fol.ex A p) --> ex A (x : term A => subst_prop s (p x))
[s,p,l] subst_prop s (fol.apply_pred p l) -->
apply_pred p (subst_terms s (pred_arity p) l).
apply_pred p (subst_terms s (pred_domain p) l).
[] subst_terms _ _ fol.nil_term --> nil_term
[s,B,b,Bs,bs] subst_terms s _ (fol.cons_term B b Bs bs) -->
cons_term B (subst_term s B b) Bs (subst_terms s Bs bs).
[s,f,l] subst_term s _ (fol.apply_fun f l) -->
apply_fun f (subst_terms s (fun_arity f) l).
apply_fun f (subst_terms s (fun_domain f) l).
(; Until here, the subst functions are identities only defined on
close terms. To get a real substitution behaviour, we add a
......@@ -168,7 +168,7 @@ def bor : bool -> bool -> bool.
def occur : A : sort -> term A -> B : sort -> term B -> bool.
def occur_terms : A : sort -> term A -> Bs : sorts -> terms Bs -> bool.
[x] occur _ x _ x --> btrue
[A,x,f,l] occur A x _ (fol.apply_fun f l) --> occur_terms A x (fun_arity f) l
[A,x,f,l] occur A x _ (fol.apply_fun f l) --> occur_terms A x (fun_domain f) l
[] occur _ _ _ _ --> bfalse.
[] occur_terms _ _ _ fol.nil_term --> bfalse
[A,x,B,b,Bs,bs]
......@@ -180,7 +180,7 @@ def unify_occur : unify_problem -> A : sort -> term A -> term A -> bool -> unify
def subst_in_unify_problem : A : sort -> term A -> term A -> unify_problem -> unify_problem.
[] unify unify_nil --> unify_success empty_subst
[f,l,l',pb] unify (unify_cons _ (fol.apply_fun f l) (fol.apply_fun f l') pb) -->
unify (unify_cons_terms (fun_arity f) l l' pb)
unify (unify_cons_terms (fun_domain f) l l' pb)
[] unify (unify_cons _ (fol.apply_fun _ _) (fol.apply_fun _ _) _) --> unify_failure
[a,pb] unify (unify_cons _ a a pb) --> unify pb
[A,f,l,x,pb] unify (unify_cons A (fol.apply_fun f l) x pb) --> unify (unify_cons A x (apply_fun f l) pb)
......@@ -211,15 +211,15 @@ def unify' (pb : unify_problem) :=
A : sort.
f : function.
[] fol.fun_arity f --> read_sorts (nat.S (nat.S nat.O)) A A.
[] fol.fun_domain f --> read_sorts (nat.S (nat.S nat.O)) A A.
[] fol.fun_codomain f --> A.
a : function.
[] fol.fun_arity a --> read_sorts nat.O.
[] fol.fun_domain a --> read_sorts nat.O.
[] fol.fun_codomain a --> A.
b : function.
[] fol.fun_arity b --> read_sorts nat.O.
[] fol.fun_domain b --> read_sorts nat.O.
[] fol.fun_codomain b --> A.
x : term A.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment