anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-08 16:51:53 +03:00
Code Issues Projects Releases Wiki Activity
54d6c28127
juvix/docs/org/explanations/totality/termination.org
Łukasz Czajka b95abeaada
Restructure the documentation and add a tutorial (#1718) 
* Closes #1597 
* Closes #1624 
* Closes #1633 

The tutorial uses syntax which has not been implemented yet: it depends
on
- #1637, 
- #1716, 
- #1639,
- #1638.

The tutorial also assumes the following issues are done: 
- #1720, and
- #1701.

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-01-19 13:28:21 +01:00

1.1 KiB
Raw Blame History

Termination

To not bring inconsistencies by function declarations, Juvix requires that every function passes its termination checker. However, since this is a strong requirement, often tricky to fulfill, we give the user the possibility to skip this check in two different ways:

  • Using the terminating keyword to annotate function type signatures as terminating. The syntax is the following.
terminating fun : A → B;

Note that annotating a function as terminating means that all its function clauses pass the termination checker's criterion. To skip the termination checker for mutual recursive functions, all the functions involved must be annotated as terminating.

  • Using the CLI global flag --no-termination.
juvix typecheck --no-termination MyProgram.juvix

In any case, be aware that our termination checker is limited as it only accepts a subset of recursion functions. The termination checker algorithm is a slightly modification of the algorithm for checking termination in the Foetus's language.