Dependent types have been used at the core of many proof assistants, and more recently there have been efforts to extend their use to functional programming languages. Dependent type theories allow programming and reasoning in a common framework.
The pattern matching notation, known from traditional programming, has been proposed for defining recursive functions in such systems. While pattern matching is intuitive and powerful, it has to be ensured that the defined functions are total.
One aspect of totality is termination: the evaluation of a function at any argument must be computable in finite time. Infinite objects can be added to the language by computing only finite parts of them as necessary. Valid definitions of infinite objects need to be productive.
As the halteproblem is undecidable, the goal can only be to accept as many valid definitions as possible. There are many approaches to ensure termination. One is to allow the definition of functions where the recursive calls follow a certain scheme. The size-change principle subsumes some of these schemes.
Another approach is the use of sized types, where information about the height of arguments is tracked in the type system and is used to recognize definitions as terminating.
For this thesis, the system Mugda was developed and will subsequently be described. It is based on Martin-Löf type theory and supports inductive and coinductive types. Recursive functions are defined by pattern matching. Its termination criterion is based on the size-change principle. In addition, the language provides elements to enable the use of sized types.
Download the source code for Mugda with examples (mugda.tar.gz). For more on the implementation of Mugda, see the appendix of the diploma thesis.