@@ -99,6 +99,30 @@ the difference between:
9999 Idris> \n, m => n + (S m)
100100 \n => \m => plus n (S m) : Nat -> Nat -> Nat
101101
102+I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
103+=============================================================================================
104+
105+Idris can't decide in general whether a program is terminating due to
106+the undecidability of the `Halting Problem
107+<https://en.wikipedia.org/wiki/Halting_problem>`_. It is possible, however,
108+to identify some programs which are definitely terminating. Idris does this
109+using "size change termination" which looks for recursive paths from a
110+function back to itself. On such a path, there must be at least one
111+argument which converges to a base case.
112+
113+- Mutually recursive functions are supported
114+- However, all functions on the path must be fully applied. In particular,
115+ higher order applications are not supported
116+- Idris identifies arguments which converge to a base case by looking for
117+ recursive calls to syntactically smaller arguments of inputs. e.g.
118+ ``k`` is syntactially smaller than ``S (S k)`` because ``k`` is a
119+ subterm of ``S (S k)``, but ``(k, k)`` is
120+ not syntactically smaller than ``(S k, S k)``.
121+
122+If you have a function which you believe to be terminating, but Idris does
123+not, you can either restructure the program, or use the ``assert_total``
124+function.
125+
102126When will Idris be self-hosting?
103127================================
104128