coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pablo Argon <pargon AT cadence.com>
- To: coq-club <coq-club AT pauillac.inria.fr>
- Cc: Ken McMillan <mcmillan AT cadence.com>
- Subject: "Warning: Ignoring recursive call" and Recursive Functions
- Date: Wed, 06 Sep 2000 11:15:13 -0700
- Organization: INRIA & Cadence Berkeley Laboratories
Hello Coq team and users,
here follows 2 or three questions close related.
I want to formalize a set of formulas; formulas are built from
a set of operators (Oper), where each operator has an arity (>= 0).
At this point I don't want to fix a syntax, nevertheless I
want to reason about this set of objects.
So, my first attempt was to say:
-----------------------------------------------------
Variable Oper :Set.
Variable Denotation:Set.
Variable Arity : Oper -> nat.
Inductive fla : Set :=
fla_intro : (f:Oper)(l:(list fla))fla .
------------------------------------------------------
First question: What means Coq's message:
"Warning: Ignoring recursive call"
given by this inductive definition ?
This formalization seems to work well, even if I
theoretically I want to ensure that (length l)=(Arity o).
(Note that non positiveness of:
Inductive fla : Set :=
fla_intro : (f:Oper)(l:(list fla)) (length l)=(Arity f)->fla .
even if I can't see any "unsoundness" introduced by this definition)
I can define the denotation of a formula
given a function OpInterpretation, in Coq:
------------------------------------------------------
Variable OpInterpretation : Oper -> (list Denotation) -> Denotation.
Fixpoint FlaDenot_1 [ fx : fla] : Denotation :=
Cases fx of
(fla_intro f l)=> (OpInterpretation f (map FlaDenot_1 l))
end.
------------------------------------------------------
I was very surprise that Coq accepts this definition...
it seems to open the door for non-terminating functions !?
(cf. message from Maria Joao Frade on Jul/03/00 ?)
Note that the inductive scheme for the type fla
synthesized by Coq is not powerful enough...
but we can prove by hand the correct one.
Then, my second attempt was (merci Bruno):
------------------------------------------------------
Variable Oper :Set.
Variable Arity : Oper -> nat.
Mutual Inductive flaN : Set :=
fla_n : (o:Oper)(l:(listf (Arity o)))flaN
with
listf : nat -> Set :=
nilfla : (listf O)
| consfla : (n:nat)flaN -> (listf n) -> (listf (S n)).
Scheme fla_ind2 := Induction for flaN Sort Prop
with listf_ind2 := Induction for listf Sort Prop.
------------------------------------------------------
Excellent, I have the arity test, and the induction scheme!
BUT, now I want to define the denotation of a formula
given a function OpInterpretation, in Coq:
------------------------------------------------------
Parameter Denotation : Set.
Variable OpInterpretation :
Oper -> (list Denotation) -> Denotation.
Fixpoint mapN [B: Set; fun: flaN ->B ; n:nat; l:(listf n)] : (list B) :=
Cases l of
nilfla => (nil B)
| (consfla m fh ft)=> (cons (fun fh) (mapN B fun m ft))
end.
Fixpoint FlaDenotation [ fl : flaN] : Denotation :=
Cases fl of
(fla_n o lf)=> (OpInterpretation o (mapN Denotation FlaDenotation
(Arity o) lf))
end.
------------------------------------------------------
The last definition rises the error:
Error during interpretation of command:
Fixpoint FlaDenotation [ fl : flaN] : Denotation :=
Cases fl of (fla_n o lf)=> (OpInterpretation o (mapN Denotation
FlaDenotation (Arity o) lf)) end.
Error: Not enough arguments for the recursive call
The recursive definition FlaDenotation :=
[fl:flaN]
Cases fl of
(fla_n o lf) =>
(OpInterpretation o (mapN Denotation FlaDenotation (Arity o) lf))
end is not well-formed
Why this time Coq aware of the unsoundness of the definition and not in
the
former case?
Thank you all in advance for you help and/or advice,
Pablo
PS: Follows the full script (Question.v) and an
instantiation to play with (Question_Example.v).Require Export PolyList.
Section Formulas.
Variable Oper :Set.
Variable Denotation:Set.
Inductive fla : Set :=
fla_intro : (f:Oper)(l:(list fla))fla .
Variable OpInterpretation : Oper -> (list Denotation) -> Denotation.
Fixpoint FlaDenot_1 [ fx : fla] : Denotation :=
Cases fx of
(fla_intro f l)=> (OpInterpretation f (map FlaDenot_1 l))
end.
End Formulas.
Section FormulasNAire.
Variable Oper :Set.
Variable Arity : Oper -> nat.
Mutual Inductive flaN : Set :=
fla_n : (o:Oper)(l:(listf (Arity o)))flaN
with
listf : nat -> Set :=
nilfla : (listf O)
| consfla : (n:nat)flaN -> (listf n) -> (listf (S n)).
Scheme fla_ind2 := Induction for flaN Sort Prop
with listf_ind2 := Induction for listf Sort Prop.
Parameter Denotation : Set.
Variable OpInterpretation :
Oper -> (list Denotation) -> Denotation.
Fixpoint mapN [B: Set; fun: flaN ->B ; n:nat; l:(listf n)] : (list B) :=
Cases l of
nilfla => (nil B)
| (consfla m fh ft)=> (cons (fun fh) (mapN B fun m ft))
end.
(* *)
Fixpoint FlaDenotation [ fl : flaN] : Denotation :=
Cases fl of
(fla_n o lf)=> (OpInterpretation o (mapN Denotation FlaDenotation
(Arity o) lf))
end.
(* Error during interpretation of command:
Fixpoint FlaDenotation [ fl : flaN] : Denotation :=
Cases fl of (fla_n o lf)=> (OpInterpretation o (mapN Denotation
FlaDenotation (Arity o) lf)) end.
Error: Not enough arguments for the recursive call
The recursive definition FlaDenotation :=
[fl:flaN]
Cases fl of
(fla_n o lf) =>
(OpInterpretation o (mapN Denotation FlaDenotation (Arity o) lf))
end is not well-formed
*)
End FormulasNAire.
Require Question.
Section Example. (* petit langage booleen *)
Inductive Oper : Set :=
TT : Oper
|FF : Oper
|nnot : Oper
|aand : Oper.
Definition Arity [o:Oper] :nat :=
Cases o of
TT => O
|FF => O
|nnot => (S O)
|aand => (S (S O))
end.
(* let's give a tri-valued denotation *)
Inductive boolF : Set :=
vrai : boolF | faux : boolF | bottom : boolF.
Definition OperInterp [o:Oper ; l:(list boolF) ] : boolF :=
Cases o of
TT => vrai
|FF => faux
|nnot => Cases l of
nil => bottom
|(cons v tl) => Cases v of
vrai => faux
| faux => vrai
| bottom => bottom
end
end
|aand => Cases l of
nil => bottom
|(cons v tl) => Cases v of
vrai => Cases tl of
nil => bottom
|(cons v tll) => Cases v of
vrai =>
vrai
| faux =>
faux
| bottom =>
bottom
end
end
| faux => faux
| bottom => bottom
end
end
end.
(* Examples of formulas with arity check *)
Definition phiTT :=(fla_n Oper Arity TT (nilfla ? ?)).
Definition phi1 := (fla_n Oper Arity nnot (consfla ? ? O phiTT
(nilfla ? ?))).
(* Examples of formulas without arity check *)
Definition phiT :=(fla_intro Oper TT (nil (fla Oper))).
Definition phi2 := (fla_intro Oper nnot (cons phiT (nil (fla Oper)))).
Definition phi3 := (fla_intro Oper aand (cons phi2 (cons phiT (nil (fla
Oper))))).
Definition SemBoolF[f:(fla Oper)] := (FlaDenot_1 Oper boolF OperInterp f).
Eval Compute in (SemBoolF phi2).
Eval Compute in (SemBoolF phi3).
Eval Compute in (SemBoolF (fla_intro Oper nnot (nil (fla Oper)))).
- "Warning: Ignoring recursive call" and Recursive Functions, Pablo Argon
Archive powered by MhonArc 2.6.16.