Recursive Functions with Higher Order Domains

In a series of articles, we developed a method to translate general recursive functions written in a functional programming style into constructive type theory. Three problems remained: the method could not properly deal with functions taking functional arguments, the translation of terms containing λ-abstractions was too strict, and partial application of general recursive functions was not allowed. Here, we show how the three problems can be solved by defining a type of partial functions between given types. Every function, including arguments to rder functions, λ-abstractions and partially applied functions, is then translated as a pair consisting of a domain predicate and a function dependent on the predicate. Higher order functions are assigned domain predicates that inherit termination conditions from their funcrguments. The translation of a λ-abstraction does not need to be total anymore, but generates a local termination condition. The domain predicate of a partially applie...

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: Ana Bove, Venanzio Capretta
• Keywords: Domain Predicate, General Recursive Functions, Recursive Functions, Theoretical Computer Science, TLCA 2005