### Skapa referens, olika format (klipp och klistra)

**Harvard**

Bove, A. och Capretta, V. (2007) *Computation by Prophecy*.

** BibTeX **

@conference{

Bove2007,

author={Bove, Ana and Capretta, Venanzio},

title={Computation by Prophecy},

booktitle={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 )},

isbn={978-3-540-73227-3},

pages={70--83},

abstract={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.},

year={2007},

keywords={type theory, general recursion, partial functions},

}

** RefWorks **

RT Conference Proceedings

SR Print

ID 47397

A1 Bove, Ana

A1 Capretta, Venanzio

T1 Computation by Prophecy

YR 2007

T2 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 )

SN 978-3-540-73227-3

SP 70

AB 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.

LA eng

OL 30