patternMinor
Decidability of dependent typing on primitive recursive languages
Viewed 0 times
languagesprimitiverecursivetypingdecidabilitydependent
Problem
With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this: would an implementation of dependent typing for a primitive recursive language(not Turing-complete) be guaranteed to halt? Thanks!
Solution
Not only is the answer to this question yes, but this is exactly the strategy that modern implementations like Coq and Agda take! To be precise, the type checker has to preform evaluation when deciding definitional equality so it would, if given the right language, be possible to write an infinite loop and ask whether a term was definitionally equal to another term. Because of the way we define definitional equality in most cases, this demands evaluation.
The calculus of constructions (CoC) is actually strongly normalizing. Type checking of CoC is decidable and requires no termination checking. But to make this theory more useful, we add the ability to define inductive types and recursions over them. This way, we get the calculus of inductive constructions (CIC), which Coq is based on. You can view this as a means of adding terms to our language which add computational content that would otherwise not be present.
Note than many inductive types can already be represented in CoC without the aid of CIC, but CoC cannot represent everything CIC can. Coq and Agda both have termination checkers which accept all primitive recursive functions, and both also allow encoding the Ackermann function. You can see more about this in a question I once asked here on a characterization of the class of primitive recursive functions.
Good refrences on Agda's termination checker are
There is also a lot of work on sized types to provide an alternative to termination checking as well as some work on abstract interpretation based solutions. Currently however, checking for a generalization (see Foetus) of primitive recursion is as far as the state of the art in mainstream implementations goes — at least as far as I am aware.
The calculus of constructions (CoC) is actually strongly normalizing. Type checking of CoC is decidable and requires no termination checking. But to make this theory more useful, we add the ability to define inductive types and recursions over them. This way, we get the calculus of inductive constructions (CIC), which Coq is based on. You can view this as a means of adding terms to our language which add computational content that would otherwise not be present.
Note than many inductive types can already be represented in CoC without the aid of CIC, but CoC cannot represent everything CIC can. Coq and Agda both have termination checkers which accept all primitive recursive functions, and both also allow encoding the Ackermann function. You can see more about this in a question I once asked here on a characterization of the class of primitive recursive functions.
Good refrences on Agda's termination checker are
- http://www2.tcs.ifi.lmu.de/~abel/foetus/
- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker
There is also a lot of work on sized types to provide an alternative to termination checking as well as some work on abstract interpretation based solutions. Currently however, checking for a generalization (see Foetus) of primitive recursion is as far as the state of the art in mainstream implementations goes — at least as far as I am aware.
Context
StackExchange Computer Science Q#53130, answer score: 6
Revisions (0)
No revisions yet.