Stream: Coq users

Topic: Termination Checker for Nested Lists

Josh Cohen (Apr 19 2024 at 19:57):

Hello, I am confused about the behavior of Coq's termination checker on nested lists. Namely, in the following example, termination checking fails:

Fixpoint map2' {A B C: Type} (f : A -> B -> C) (l1 : list A) (l2: list B) : list C :=
  match l1, l2 with
  | x1 :: t1, x2 :: t2 => f x1 x2 :: map2' f t1 t2
  | _, _ => nil
  end.

Inductive tree : Type :=
  | Leaf : nat -> tree
  | Node : list tree -> tree.

Fail Fixpoint tree_eqb1 (t1 t2: tree) {struct t1} : bool :=
  match t1, t2 with
  | Leaf n1, Leaf n2 => Nat.eqb n1 n2
  | Node l1, Node l2 => Nat.eqb (length l1) (length l2) &&
    forallb id (map2' tree_eqb1 l1 l2)
  | _, _ => false
  end.

It fails with message "Recursive call to tree_eqb1 has not enough arguments".

But if I write map2 in a more unusual (but equivalent) way, termination checking succeeds:

Definition map2 {A B C: Type} :=
  fun (f: A -> B -> C) =>
    fix map2 (l1: list A) : list B -> list C :=
      match l1 with
      | nil => fun l2 => nil
      | x1 :: t1 =>
        fun l2 =>
        match l2 with
        | nil => nil
        | x2 :: t2 => f x1 x2 :: map2 t1 t2
        end
      end.

 Fixpoint tree_eqb2 (t1 t2: tree) {struct t1} : bool :=
  match t1, t2 with
  | Leaf n1, Leaf n2 => Nat.eqb n1 n2
  | Node l1, Node l2 => Nat.eqb (length l1) (length l2) &&
    forallb id (map2 tree_eqb2 l1 l2)
  | _, _ => false
  end.

Does anyone know why this is the case?

Guillaume Melquiond (Apr 20 2024 at 03:43):

You don't need to make map2 so ugly. The only thing that matters here is that its argument f be outside the fixed point (i.e., be visibly constant across the iterations of map2). Other than that, you can write map2 the usual way. (In particular, if you were using Section to lift f, it would be written exactly the usual way.) As to why the termination checker does not support this case, I am not quite sure.

Dominique Larchey-Wendling (Apr 20 2024 at 06:21):

There is indeed a very subtle aspect of the guard checker. It already manifests itself already on the simpler case of map on rose trees below

Require Import List.

Fixpoint map_int {X Y} (f : X -> Y) l :=
  match l with
  | nil  => nil
  | x::l => f x :: map_int f l
  end.

Definition map_ext {X Y} (f : X -> Y) :=
  fix loop l :=
    match l with
    | nil  => nil
    | x::l => f x :: loop l
    end.

Inductive tree X :=
  | node : X -> list (tree X) -> tree X.

Arguments node {_}.

Fixpoint map_ext_tree {X Y} (f : X -> Y) t :=
  match t with
  | node x l => node (f x) (map_ext (map_ext_tree f) l)
  end.

Fail Fixpoint map_int_tree {X Y} (f : X -> Y) t { struct t } :=
  match t with
  | node x l => node (f x) (map_int (map_int_tree f) l)
  end.

The terms map_int and map_ext look nearly interchangeable, but they are not from the guard-checker point of view. Indeed:

• in map_ext_tree, the sub-term map_ext (map_ext_tree f) can be reduced to fix loop l := match l with nil => nil | x::l => map_ext_tree f x :: loop l end because map_ext is a Definition. And this type-checks as a nested-fixpoint;
• in map_int_tree, the sub-term map_int (map_ext_tree f) l cannot be reduced further because map_int is a Fixpoint and its struct argument, hence l here, must first be reduced to a term with a head constructor to further reduce the fixpoint. Not the case in the code of map_int_tree.

Pierre-Marie Pédrot (Apr 20 2024 at 06:48):

FTR I think that this discrepancy would be fixed by https://github.com/coq/coq/pull/17986 whose purpose is precisely to check guard as if the parameters were extruded.

Last updated: Oct 13 2024 at 01:02 UTC