[Agda] Checking termination is not sufficiently exploratory.

[Robbert Krebbers]

On 2018-07-31 03:19, Jason -Zhong Sheng- Hu wrote:
> I am wondering if there is any implementation of dependent type
> theory performs normalization before termination checking?
Coq is doing exactly that, the example of Serge is thus happily accepted 
by Coq, see below for a version of his example in Coq.

Note that while performing normalization before termination checking 
provides extra flexibility, it brings other problems---The following 
program is accepted by Coq's termination checker but diverges when 
executed using eager evaluation:

   Fixpoint foo (n : nat) : nat :=
     let _ := foo n in
     0.
   Eval compute in foo 0.
   (* Stack overflow. *)

The problem here is that normalization removes the recursive call, which 
makes the termination checker accept the definition.

Best,

Robbert

-----------

Require Import List Ascii String.
Open Scope string_scope.

CoInductive costring := snil | scons : ascii -> costring -> costring.

Fixpoint sapp (xs : string) (ys : costring) : costring :=
   match xs with
   | "" => ys
   | String x xs => scons x (sapp xs ys)
   end.

CoFixpoint cosplit'' (xs : costring) : costring :=
   match xs with
   | snil => snil
   | scons x xs =>
      if ascii_dec x "!" then scons x (cosplit'' xs)
      else sapp ">>" (cosplit'' xs)
   end.