Fix docs

doc/user-manual/language/type-based-termination-checking.rst

@@ -11,6 +11,9 @@
 Type-Based Termination Checking
 *******************************
 
+.. note::
+   Type-based termination checking is based on a master's thesis described in :ref:`[1]<type-based-termination-checking-references>`.
+
 Sometimes the default termination checker in Agda may seem too weak. Let's explore this in the context of defining a finitely-branching tree:
 
 ::
@@ -25,7 +28,7 @@ Intuitively, we observe that ``children`` represents a list of "smaller" rose tr
 
 However, ``mapRose`` does not adhere to the pattern of syntactic recursion, as it is passed to another function instead of being directly called on a structurally smaller argument. Agda rejects such definitions because, instead of ``map``, an arbitrary function could be used. This arbitrary function might alter its arguments in unpredictable ways, rendering ``mapRose`` non-terminating.
 
-In our case, we use ``map`` and trust it. The evidence for this trust lies in the type signature of ``map: {A' B' : Set} → (A' → B') → List A' → List B'``. According to this signature, map operates on arbitrary types, meaning it cannot construct a malicious ``RoseTree``. This property, known as parametricity, aligns with the logic of Agda, as described in :ref:`[1]<type-based-termination-checking-references>`.
+In our case, we use ``map`` and trust it. The evidence for this trust lies in the type signature of ``map: {A' B' : Set} → (A' → B') → List A' → List B'``. According to this signature, map operates on arbitrary types, meaning it cannot construct a malicious ``RoseTree``. This property, known as parametricity, aligns with the logic of Agda, as described in :ref:`[2]<type-based-termination-checking-references>`.
 
 The idea of the type-based termination checker is that Agda can try to track
 the "sizes" of terms, and deduce whether the recursive calls eventually happen on
@@ -127,6 +130,97 @@ Now consider the following function:
 
 The difference here is that now inner ``badRepeat`` is projected. The logic from the previous paragraph does not apply here: if ``badRepeat .tail`` is of depth ``m``, then the inner ``badRepeat`` must have depth bigger than ``m``, say ``k``. There is no evidence that ``k < n``, so Agda rejects this definition as non-terminating. Indeed, it can be unfolded infinitely, which destroys strong normalization.
 
+.. _type-based-termination-checking-mutual-induction-coinduction:
+
+Induction-Coinduction
+-----------------------
+
+One of the features of the type-based termination checker is the support of mutually defined inductive and coinductive types.
+
+We shall illustrate it on the stream processors.
+
+::
+
+    -- The inductive part of stream processors
+    -- This datatype allows choosing to consume incoming stream or
+    -- produce an element of a new one.
+    data   SPμ (A B : Set) : Set
+    -- The coinductive part of stream processors
+    -- This datatype carries infinite behavior of this class.
+    record SPν (A B : Set) : Set
+
+    data SPμ A B where
+      get : (A → SPμ A B) → SPμ A B -- Consumes an element of the incoming stream
+      put : B → SPν A B → SPμ A B   -- Produces an element of the constructed stream
+
+    record SPν A B where
+      coinductive
+      field force : SPμ A B
+
+    open SPν
+
+This datatype can be understood differently depending on the order of fixpoint operators in its formal definition. The two meanings that can be given here are
+``ν SPν. μ SPμ. (A → SPμ) + (B ⨯ SPν)`` and ``μ SPμ. ν SPν. (A → SPμ) + (B ⨯ SPν)``. There is a substantial difference here. The first interpretation means that the stream processor infinitely produces ``B``, consuming a finite number of ``A``s between two productions. The second interpretation means that the stream processor may consume only finite number of ``A``s, and between each two consumptions it is allowed to produce infinite number of ``B``s. It is natural to select the first interpretation for stream processors, and that's what the type-based termination checker does.
+
+This behavior can be reflects with the use of Agda's sized types:
+
+::
+
+    data   SPμ (i j : Size) (A B : Set) : Set
+    record SPν (i : Size) (A B : Set) : Set
+
+    data SPμ i j A B where
+      get : {k : Size< j} → (A → SPμ i k A B) → SPμ i j A B
+      put : B → SPν i A B → SPμ i j A B
+
+    record SPν i A B where
+      coinductive
+      field force : {k : Size< i} → SPμ k ∞ A B
+
+The following functions pass termination checking. We shall explain why ``runSPμ`` is a terminating function.
+
+::
+
+    runSPμ : {A B : Set} → SPμ A B → Stream A → Stream B
+    runSPμ (put b spν) s .hd = b
+    runSPμ (put b spν) s .tl = runSPμ (SPν.force spν) s
+    runSPμ (get f) s = runSPμ (f (s .hd)) (s .tl)
+
+    runSPν : {A B : Set} → SPν A B → Stream A → Stream B
+    runSPν spν s = runSPμ (SPν.force spν) s
+
+
+In the second clause, the list of copatterns contains a coinductive projection ``tl``. This means that if ``runSPμ`` defines a stream of depth ``n``, then the body ``runSPμ (SPν.force spν) s`` must define a stream of depth ``m < n``. Since ``runSPμ`` is not wrapped into any projection, Agda assumes that this corecursive call defines a stream of depth ``m``, which means that this clause cannot be unfolded infinitely.
+
+In the third clause, there are no coinductive projections among copatterns. If ``runSPμ`` defines a stream of depth ``n``, here Agda assumes that ``runSPμ (f (s .hd)) (s .tl)`` also defines a stream of depth ``n``. This fact alone is not enough to prove termination: after all, the definition of ``runSPμ`` can be unfolded to the third clause infinitely, since ``n`` does not decrease during unfolding. However, ``runSPμ`` has also an inductive argument, which decreases with each call. It means that the third clause preserves the depth of the defined stream, but it decreases the inductive size of the accepted ``SPμ``.
+
+Now we see that the unfolding of the first clause strictly decreases the depth of the stream, and the unfolding of the second clause preserves the depth of the stream, but strictly decreases the inductive size of ``SPμ``. This kind of lexicographical induction allows Agda to deduce that ``runSPμ`` terminates.
+
+In general, if there is a set of mutually-inductive-coinductive datatypes, then the type-based checker provides the following encoding for them: there is a common size variable for all definitions that corresponds to coinductive part of the definition, and this variable can be decreased only by a coinductive projection. For inductive datatypes, there is additionally another size variable, that corresponds to the inductive part of the definition, and it can be decreased only by pattern-matching on an inductive constructor. This encoding can be represented in terms of Agda's sized types:
+
+::
+    data D1 (i j : Size) ... : ... → Set
+    data D2 (i j : Size) ... : ... → Set
+    ...
+    data Dn (i j : Size) ... : ... → Set
+    data R1 (i : Size)   ... : ... → Set
+    data R2 (i : Size)   ... : ... → Set
+    data Rm (i : Size)   ... : ... → Set
+
+    data D i j ... where
+      c1 : {j' : Size< j} → ... → Dk i j' → ... → D i j ...
+      c2 : ... → Rk i → ... → D i j ...
+      ...
+
+    record Rn i ... where
+      coinductive
+      field
+      f1 : {i' : Size< i} → ... → Rk i'
+      f2 : {i' : Size< i} → ... → Dk i' ∞
+      ...
+
+
+
 .. _type-based-termination-checking-size-preservation:
 
 Size preservation
@@ -204,7 +298,7 @@ As a final note, we address performance considerations. Currently, size-preserva
 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:`[2]<type-based-termination-checking-references>`.
+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>`.
 
 The semantical framework used in the type-based termination checker is a variant of *sized types*. However, the sized types in Agda do not interact with the type-based termination checker. This stems partly from the complexity and unsoundness of sized types, whereas the type-based termination checker utilizes an intentionally restricted version of them. Presently, sized types serve as a means to manually address termination issues, although there are plans for the potential for interaction between type-based termination and sized types in the future.
 
@@ -213,8 +307,11 @@ The semantical framework used in the type-based termination checker is a variant
 References
 ----------
 
-[1] Philip Wadler -- `Theorems for free!
+[1] Kanstantsin Nisht -- `Type-Based Termination Checking in Agda.
+<https://knisht.github.io/agda/msc.pdf`_
+
+[2] Philip Wadler -- `Theorems for free!
 <https://www.cse.chalmers.se/~abela/lehre/SS07/Typen/wadler89theorems.pdf>`_
 
-[2] Andreas Abel, Brigitte Pientka -- `Well-founded recursion with copatterns and sized types.
+[3] Andreas Abel, Brigitte Pientka -- `Well-founded recursion with copatterns and sized types.
 <https://www.cambridge.org/core/journals/journal-of-functional-programming/article/wellfounded-recursion-with-copatterns-and-sized-types/39794AEA4D0F5003C8E9F88E564DA8DD>`_

src/full/Agda/Termination/TypeBased/Patterns.hs

@@ -131,7 +131,7 @@ matchLHS tele patterns = do
         freshenedSignature <- freshenCopatternProjection newCodepthVar bounds tele
         -- Additional argument is needed because we want to get rid of the principal argument in the signature
         -- This is application that is intended to get rid of the basic record arguments
-        let appliedProjection = case codom of 
+        let appliedProjection = case codom of
               UndefinedSizeType -> UndefinedSizeType
               _ -> applyDataType ((map snd recordArgs) ++ [UndefinedSizeType]) freshenedSignature
         -- TODO: handle copying here,