Termination¶
To prevent inconsistencies arising from function declarations, Juvix mandates that every function passes its termination checker. Nevertheless, this requirement can be challenging to meet; thus, we provide users with two distinct methods for bypassing this check:
Keyword¶
Utilize the terminating keyword to annotate function type signatures as terminating. In the following example we mark the function fun as terminating.
terminating
fun : A → B;
Note
Annotating a function with the terminating keyword indicates that all of its function clauses meet the termination checker's criteria. For mutual recursive functions, to bypass the termination checker, all involved functions must be annotated as terminating.
CLI flag¶
You can disable the termination checking by utilizing the global CLI flag
--no-termination.
juvix --no-termination typecheck MyProgram.juvix
Note
Please note that our termination checker has certain limitations, as it only accepts a subset of recursive functions. The algorithm used in the termination checker is a minor adaptation of the one employed for checking termination in the Foetus language.