Skip to Content.
Sympa Menu

coq-club - "Warning: Ignoring recursive call" and Recursive Functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

"Warning: Ignoring recursive call" and Recursive Functions


chronological Thread 
  • 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)))).


Archive powered by MhonArc 2.6.16.

Top of Page