The following program that does structural recursion on termination predicates (in this case the graphs of the original functions) is not accepted:

It would also be a nice candidate for doing Brady style optimisation during compilation to erase the termination predicate. This should then yield the original recursive functions as the compiled version.

Here is a simplified version of the program:

module Comb where infixr 50 _→_ data Ty : Set where ι : Ty _→_ : Ty -> Ty -> Ty data Tm : Ty -> Set where _$_ : {σ τ : Ty} -> Tm (σ → τ) -> Tm σ -> Tm τ data Nf : Ty -> Set where data _⇓_ : {σ : Ty} -> Tm σ -> Nf σ -> Set where r$ : {σ τ : Ty} -> {t : Tm (σ → τ)} -> {f : Nf (σ → τ)} -> t ⇓ f -> {u : Tm σ} -> {a : Nf σ} -> u ⇓ a -> {v : Nf τ} -> t $ u ⇓ v nf⁼ : {σ : Ty} -> (t : Tm σ) -> {n : Nf σ} -> t ⇓ n -> Set nf⁼ .{τ} (_$_ {σ} {τ} t u) {v} (r$ {f = f} p q) with nf⁼ {σ → τ} t {f} p nf⁼ (t $ u) (r$ p q) | _ = Ty

The call graph computed for nf⁼ in Termination.TermCheck is the following one:

[ [Unknown, Unknown, Unknown, Unknown] , [Unknown, Unknown, Unknown, Unknown] , [Unknown, Lt, Unknown, Unknown] , [Unknown, Unknown, Le, Unknown] ]

However, it should be this one:

[ [Unknown, Unknown, Unknown, Unknown] , [Unknown, Lt, Unknown, Unknown] , [Unknown, Unknown, Lt, Unknown] , [Unknown, Unknown, Unknown, Lt ] ]

Update: Fixed. There was a bug when generating with function calls.

Page last modified on June 04, 2007, at 01:48 PM

Powered by
PmWiki