Add type-based termination checker #7152
Conversation
knisht
added
termination
|
Regarding #1209: my termination checker does not permit these functions. For example, in #1209 (comment), the problematic function looks like inh : Stream D
force inh = lim inh , inh
|
|
Can you also elaborate on interactions with |
|
I am not aware of any problems connected with As for #5910: the pattern-matching on My termination checker also correctly rejects #3883 (comment), because it does not consider Thank you for the comments, I think it makes sense to also clarify them in the user manual. |
|
Discussion Agda dev meeting 2024-03-24.
|
CHANGELOG.md
Outdated
| @@ -56,6 +56,26 @@ Additions to the Agda syntax. | |||
| As in a `with`, multiple bindings can be separated by a `|`, and variables to | |||
| the left are in scope in bindings to the right. | |||
|
|
|||
| * Type-based termination checker | |||
|
|
|||
| Agda is now able to understand polymorphic functions during checking for structural recursion. | |||
There was a problem hiding this comment.
It's not clear to me what it means to "understand polymorphic functions", could you give a concrete example of what's the benefit here (apart from size preservation)?.
| qsort cmp (cons x xs) = qsort cmp (filter (cmp x) xs) ++ cons x (qsort cmp (filter (λ y → cmp y x) xs)) | ||
| ``` | ||
|
|
||
| Type-based termination checking also works for coinduction, which improves the guardedness predicate. |
There was a problem hiding this comment.
Again, one minimal example of something that used to fail would help here.
| @@ -1,4 +1,4 @@ | |||
| {-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-} | |||
| {-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe --type-based-termination #-} | |||
There was a problem hiding this comment.
Type-based termination is not necessary for checking the builtin files, so why did you add the flag here?
There was a problem hiding this comment.
The type-based termination checker needs to preprocess existing datatypes before using them in the actual checking process. If there is no flag, the preprocessing does not happen.
This is a behavior I would like to change: it is easy to forget to provide the flag for some definition, and then this definition will be useless for the checker. The preprocessing itself is very cheap and syntax-based, so it might make sense to enable it by default for all files. The only drawback I see here is that the preprocessing may be unstable since it is new.
There was a problem hiding this comment.
Another solution is to make --type-based-termination coinfective, which I don't like at all.
|
|
||
| Following our intuition with coinductive functions, the are three depth parameters ``k < m < n``, where the outer stream is of depth ``n``, and to pass checking the third clause should return the stream of depth at least ``k``. If the first inner ``fib`` is used with the depth ``k``, and the second ``fib`` is used with the depth ``m`` (note, that the smallest available depth for ``fib .tail`` is ``k``, hence ``fib`` must use something bigger, which is ``m``), then the size-preserving ``zipWith`` returns a stream of size ``k``, which is indeed what is required from it. Now we see that both recursive calls to ``fib`` are performed with depths ``k`` and ``m``, which are smaller than ``n``. Agda concludes that this function is terminating. | ||
|
|
||
| Size preservation is tightly coupled with polarities. Given a function signature, all occurrences of *negative inductive* and *positive coinductive* variables are considered as input, and they serve as possible candidates for size preservation analysis. On the other hand, all *positive inductive* and *negative coinductive* variables are considered as output, and a function signature may be size-preserving precisely in them. For example, consider the following definition: |
There was a problem hiding this comment.
Please expand on what you mean with negative inductive variables (etc). I know what's a negative or positive position in a type, but what does it mean for a variable to be negative or positive? Likewise, what does it mean for a variable to be inductive or coinductive?
There was a problem hiding this comment.
Ok, "variable" here is a bit of an abstraction leak, what I mean by a variable is actually a datatype. Yes, negativity and positivity refer to positions.
|
|
||
|
|
||
|
|
||
| Here, the first ``Nat`` in ``foo`` is in a doubly-negative position, which means that the position is positive, and ``foo`` can be size-preserving in the first ``Nat``. From the definition we see that it is indeed the case. One application of this fact is that the following function passes termination check: |
There was a problem hiding this comment.
What does it even mean for foo to be "size-preserving in the first Nat"? It does not produce a Nat as an output, so how could it preserve the size of it?
There was a problem hiding this comment.
This function does produce Nat as an output, the only weird thing here is that the output is in a positive position, not in a strictly positive one. As a user of foo, you can obtain this first Nat, as it is supplied by foo. On the other hand, the second Nat has to be supplied by you, and it is foo which obtains it.
| Limitations | ||
| ----------- | ||
|
|
||
| The most significant limitation of the current implementation is rooted in the fact that the size type system relies on System Fω, while the target language of Agda is dependently-typed. In cases where a type signature of a function involves large elimination, it is likely that the type-based termination checker will encounter difficulties. This limitation arises because dependent types introduce additional complexity to the underlying theory, which was initially developed for a variant of System Fω. Further details on the semantical framework can be explored in :ref:`[3]<type-based-termination-checking-references>`. |
There was a problem hiding this comment.
Could you give an example here of a situation where this problem actually shows up?
There was a problem hiding this comment.
Isn't mentioning large elimination enough? We already have an instance of this in the standard library, the reflection modules abuse large elimination, and I cannot check termination of them because of this fact.
|
The following code triggers an internal error: {-# OPTIONS --type-based-termination #-}
open import Agda.Primitive
postulate
A : Set
a : A
P : (A : Set) → A → Set
data D (_ : A) : Set where
module _ (_ _ : D a) where
record R (a : Level) (A : Set a) : Set a where
field
f : A → A
postulate
g : (A : Set) → R lzero A
module M (a : Level) (A : Set a) (r : R a A) where
h : A → A
h = R.f r
i : (A : Set) (r : R lzero A) (x : A) →
let open M lzero A r in
R lzero (P A (h x))
i A r x = g (P A _) |
Sized inference: improve handling of parameterized types Add inference of size-preservation Handle mutual recursion Support size preservation for coinductive types Allow interaction of sized and non-sized definitions Fix tests Preload sizes for each agda file Allow run only named subset of tests Extract sized primitives to a separate module to avoid conficts with --sized-types fixup makefile Add initial tests for sized inference Move instrumentation with sized arguments to internal syntax Invoke size solver on signatures of functions Support generalized variables add initial attempt to infer sizes as part of termination Add support for type generalizations Properly support system F Improve support of sized inference Adapt standard library to sized typing Further imprve termination check tmp use new size solver Rewrite size solver Improve large part of standard library tmp2 Fix handling generics in new AST Improve coverage of standard library Introduce generics with arities Improve handling of projections fully fix standard library Add encoding of axioms Support coinduction Support coinduction in stdlib Support inductive size preservation Support coinductive size preservation Fix standard library after size preservation Fix whitespace Allow running type-based and syntax-based termination checkers separately Mark builtin files as type-base-terminating Disperse implementation across several modules Refactor bidirectional checking part Refactor encoding fragment Refactor graph Refactor patterns and preservation sections Refactor definitions Remove leftovers Revert residuals 2.0 Cleanup accidental indentation Fix whitespace in tests
|
@nad I fixed this problem I also enabled preprocessing by default, as was discussed during the Agda dev meeting. |
|
Here is another problem: {-# OPTIONS --type-based-termination --no-syntax-based-termination #-}
postulate
P : (A : Set) → A → Set
f : (A : Set) (x : A) → P A x
A : Set
module M (_ : Set₁) where
record R₁ (F : Set → Set) : Set₁ where
field
x : F A
p : P (F A) x
open M Set
open R₁ ⦃ … ⦄ public
record R₂ (F : Set → Set) (A : Set) : Set where
constructor c
field
y : F A
open R₂
postulate
F : Set → Set
instance
r₁ : R₁ F
r₂ : R₁ (R₂ F)
R₁.x r₂ .y = R₁.x r₁
R₁.p r₂ = f (R₂ F A) (c x)The error message could be better. Here is a variant of the code: {-# OPTIONS --type-based-termination --no-syntax-based-termination #-}
postulate
P : (A : Set) → A → Set
f : (A : Set) (x : A) → P A x
A : Set
record R₁ (F : Set → Set) : Set₁ where
field
x : F A
p : P (F A) x
open R₁ ⦃ … ⦄ public
record R₂ (F : Set → Set) (A : Set) : Set where
constructor c
field
y : F A
open R₂
postulate
F : Set → Set
instance
r₁ : R₁ F
r₂ : R₁ (R₂ F)
R₁.x r₂ .y = R₁.x r₁
R₁.p r₂ = f (R₂ F A) (c x)Error message: This code is accepted when the regular termination checker is used. Is it expected that the new checker rejects it? |
|
Here is another problem: {-# OPTIONS --type-based-termination #-}
data F (A : Set) : Set where
c₁ : A → F A
f : (A B : Set) → (A → B) → F A → B
f _ _ g (c₁ y) = g y
mutual
data D : Set where
c₂ : D′ → D
record D′ : Set where
coinductive
field
force : D
_ : F D′ → D
_ = f D′ D c₂I encountered the problems reported above when trying to type-check code in my library with |
|
It would be great if type-based termination would also work for cubical agda which means it would need to know about PathP (as a function) but it should also mark hcomp to be size preserving (hopefully this is true unlike transp which isn't). This would mean that commutativity for CoNat is provable without using TERMINATING in the code below. {-# OPTIONS --cubical --guardedness #-}
open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Foundations.Prelude
record ℕ∞ : Set where
constructor zero-suc
coinductive
field
pred∞ : Maybe ℕ∞
open ℕ∞
zero∞ : ℕ∞
pred∞ zero∞ = nothing
suc∞ : ℕ∞ → ℕ∞
pred∞ (suc∞ m) = just m
_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
_+∞-maybe_ : Maybe ℕ∞ → ℕ∞ → Maybe ℕ∞
pred∞ (m +∞ n) = pred∞ m +∞-maybe n
nothing +∞-maybe n = pred∞ n
just m' +∞-maybe n = just (m' +∞ n)
variable l m n : ℕ∞
variable l? m? n? : Maybe ℕ∞
rneutr : m ≡ m +∞ zero∞
rneutr-maybe : m? ≡ m? +∞-maybe zero∞
pred∞ (rneutr {m = m} i) = rneutr-maybe {m? = pred∞ m} i
rneutr-maybe {m? = nothing} = refl
rneutr-maybe {m? = just m'} i = just (rneutr {m = m'} i)
lneutr : m ≡ zero∞ +∞ m
pred∞ (lneutr {m = m} i) = pred∞ m
{-# TERMINATING #-}
suc-lem : m +∞ (suc∞ n) ≡ suc∞ (m +∞ n)
suc-lem-maybe : ∀ {m n m?} → pred∞ m ≡ m? → m? +∞-maybe suc∞ n ≡ just (m +∞ n)
pred∞ (suc-lem {m = m} {n = n} i) = suc-lem-maybe {m = m}{n = n}{m? = pred∞ m} refl i
suc-lem-maybe {m = m} {n = n} {m? = nothing} q =
pred∞ (suc∞ n)
≡⟨⟩
just n
≡⟨ cong {B = λ _ → Maybe ℕ∞} just lneutr ⟩
just (zero∞ +∞ n)
≡⟨ cong {B = λ _ → Maybe ℕ∞} (λ x → just (x +∞ n)) aux ⟩
just (m +∞ n) ∎
where aux : zero∞ ≡ m
pred∞ (aux i) = q (~ i)
suc-lem-maybe {m = m} {n = n} {m? = just m'} q =
cong {B = λ _ → Maybe ℕ∞} just (
((m' +∞ suc∞ n)
≡⟨ suc-lem ⟩
suc∞ (m' +∞ n)
≡⟨ aux ⟩
m +∞ n ∎))
where aux : suc∞ (m' +∞ n) ≡ m +∞ n
pred∞ (aux i) = q (~ i) +∞-maybe n
{-# TERMINATING #-}
comm : m +∞ n ≡ n +∞ m
comm-maybe : ∀ {m n m? n?} → pred∞ m ≡ m? → pred∞ n ≡ n? → (m? +∞-maybe n) ≡ n? +∞-maybe m
pred∞ (comm {m = m} {n = n} i) = comm-maybe {m = m}{n = n}{m? = pred∞ m}{n? = pred∞ n} refl refl i
comm-maybe {m = m}{n = n}{m? = nothing}{n? = n?} p q =
pred∞ n
≡⟨ rneutr-maybe ⟩
pred∞ n +∞-maybe zero∞
≡⟨ cong (λ x → pred∞ n +∞-maybe x) aux ⟩
pred∞ n +∞-maybe m
≡⟨ cong (λ x → x +∞-maybe m) q ⟩
n? +∞-maybe m ∎
where aux : zero∞ ≡ m
pred∞ (aux i) = p (~ i)
comm-maybe {m = m}{n = n}{m? = just m'}{n? = n?} p q =
just (m' +∞ n)
≡⟨ cong {B = λ _ → Maybe ℕ∞} just (comm {m = m'}{n = n}) ⟩
just (n +∞ m')
≡⟨ sym (suc-lem-maybe {m = n}{n = m'} q) ⟩
(n? +∞-maybe (suc∞ m'))
≡⟨ cong (λ x → n? +∞-maybe x) aux ⟩
(n? +∞-maybe m) ∎
where aux : suc∞ m' ≡ m
pred∞ (aux i) = p (~ i) |
|
@knisht This PR should be rebased on latest master to updated to the latest CI, but I do not dare to do this as I might break your local copy... |
|
The following recursion through a type defined by a function does not pass the new checker. {-# OPTIONS --type-based-termination #-}
module WithTBT where
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
Tuple : (A : Set) -> Nat -> Set
Tuple A zero = ⊤
Tuple A (suc n) = Σ A \ _ -> Tuple A n
foldMap : {A : Set} (f : A -> Nat) {n : Nat} -> Tuple A n -> Nat
foldMap f {n = zero} tt = 0
foldMap f {n = suc n} (x , xs) = f x + foldMap f xs
data Tree : Set where
node : (n : Nat) -> Tuple Tree n -> Tree
tally : Tree -> Nat
tally (node n xs) = n + foldMap tally xsI can get it to work easily with {-# OPTIONS --sized-types #-}
module WithSized where
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.Size
open import Agda.Builtin.Unit
Tuple : (A : Set) -> Nat -> Set
Tuple A zero = ⊤
Tuple A (suc n) = Σ A \ _ -> Tuple A n
foldMap : {A : Set} (f : A -> Nat) {n : Nat} -> Tuple A n -> Nat
foldMap f {n = zero} tt = 0
foldMap f {n = suc n} (x , xs) = f x + foldMap f xs
data Tree (i : Size) : Set where
node : {j : Size< i} (n : Nat) -> Tuple (Tree j) n -> Tree i
tally : {i : Size} -> Tree i -> Nat
tally (node n xs) = n + foldMap tally xsI don't claim to understand the algorithm, but I think it'd be very nice if it could support this case. |
This is a technical description of the pull request.
For intro-level overview of type-based termination, consider reading user manual.
For deep semantical discussion of the process, consider reading a paper.
The development is pretty much ready to play with, and I welcome whatever tricky examples (including mutual induction-coinduction) you have.
Overview
This PR introduces three options:
--type-based-termination(disabled by default),--syntax-based-termination(enabled by default),--size-preservation(enabled by default).If a module is type-checked with
--type-based-termination, the process of encoding starts for all provided definitions. Encoding must run after polarity checking, and currently it is invoked at the beginning of the termination checking. During encoding, internal types for all definitions are converted to sized types (do not confuse them with the existing sized types of Agda; starting from now, the expression sized types refers to a separate concept local to this PR), which form a variant of System Fω. Sized types are stored alongside constants and can be serialized.If termination checking runs for a function definition under
--type-based-termination, then an alternative (to usual structural recursion) termination certificate may be produced. Each clause of the function definition is bidirectionally type-checked against the encoded sized type, where each recursive call gives rise to aCallMatrixbased on relations between sized types. As in the classic termination checker, size-change principle ensures that the function is strongly normalizing by the set of matrices.There is also a feature of size preservation, which is regulated by
--size-preservation. The implementation is roughly the following: in a function signature, each output size is attempted to be identified with each input size, obtaining a modified sized type. If the function can still be type-checked against the modified sized type, then the input and output sizes are actually the same and this information is serialized later.There should not be problematic interaction with any other feature, as in the current implementation, sized types "live in their own world", which makes the whole process similar to the double checker. Additionally, the algorithm fails if it cannot understand unusual behavior (such as pattern-matching in the presence of univalence), so it would rather not work than produce a strange termination certificate.
Performance
The measurements were taken on MacBook M2.
On the standard library, the time measurement produces the following results:
Without the type-based termination, the measurement for termination checking is
3,530ms.On graded type theory, the results are of similar proportion:
Without the type-based termination, the measurement for termination checking is
31,342ms.One important note is that for graded type theory I had to disable size preservation, which is currently implemented very naïvely. This is an area of future work.
Overall, performance impact is acceptable -- on large projects, matrix solving starts taking most of the time, but the syntax-based termination checker would also suffer from it. I suggest that, in the absence of issues with soundness, the type-based termination checker may be enabled by default in the future releases.