Computer Science – Logic in Computer Science
Scientific paper
2012-02-16
EPTCS 77, 2012, pp. 55-61
Computer Science
Logic in Computer Science
In Proceedings FICS 2012, arXiv:1202.3174
Scientific paper
10.4204/EPTCS.77.8
Bove and Capretta's popular method for justifying function definitions by general recursive equations is based on the observation that any structured general recursion equation defines an inductive subset of the intended domain (the "domain of definedness") for which the equation has a unique solution. To accept the definition, it is hence enough to prove that this subset contains the whole intended domain. This approach works very well for "terminating" definitions. But it fails to account for "productive" definitions, such as typical definitions of stream-valued functions. We argue that such definitions can be treated in a similar spirit, proceeding from a different unique solvability criterion. Any structured recursive equation defines a coinductive relation between the intended domain and intended codomain (the "coinductive graph"). This relation in turn determines a subset of the intended domain and a quotient of the intended codomain with the property that the equation is uniquely solved for the subset and quotient. The equation is therefore guaranteed to have a unique solution for the intended domain and intended codomain whenever the subset is the full set and the quotient is by equality.
No associations
LandOfFree
Structured general corecursion and coinductive graphs [extended abstract] 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 Structured general corecursion and coinductive graphs [extended abstract], we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Structured general corecursion and coinductive graphs [extended abstract] will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-124946