CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Computation by Prophecy

Ana Bove (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Venanzio Capretta
Typed Lambda Calculus and Applications; Simona Ronchi Della Rocca (Ed.), 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings. (Lecture notes in computer science; 4583 ) (0302-9743). p. 70--83. (2007)
[Konferensbidrag, refereegranskat]

We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that characterises the traces of the computation of the function. The structure of a prophecy is a possibly infinite tree, which is coerced by linearisation to a type of partial results defined by applying the delay monad to the co-domain of the function. Using induction on a weight relation defined on the prophecies, we can reason about them and prove that the formal type-theoretic version of the recursive function, resulting from the present method, satisfies the recursive equations of the original function. The advantages of this technique over the method previously developed by the authors via a special-purpose accessibility (domain) predicate are: there is no need of extra logical arguments in the definition of the recursive function; the function can be applied to any element in its domain, regardless of termination properties; we obtain a type of partial recursive functions between any two given types; and composition of recursive functions can be easily defined.

Nyckelord: type theory, general recursion, partial functions

Denna post skapades 2007-09-10. Senast ändrad 2007-09-10.
CPL Pubid: 47397


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)



Chalmers infrastruktur