General Recursion via Coinductive Types

Details General Recursion via Coinductive Types General Recursion via Coinductive Types

2005-05-13

arxiv.org/abs/cs/0505037v6

LMCS 1 (2:1) 2005

Computer Science

Logic in Computer Science

28 pages

Scientific paper

10.2168/LMCS-1(2:1)2005

A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements Partial(A), coinductively generated by two constructors: the first, return(a) just returns an element a:A; the second, step(x), adds a computation step to a recursive element x:Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.

Affiliated with

Also associated with

No associations

Rating

General Recursion via Coinductive Types does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with General Recursion via Coinductive Types, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and General Recursion via Coinductive Types will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-650045