Conference icon

Conference

Proving the Unique Fixed-Point Principle Correct An Adventure with Category Theory

Abstract:

Say you want to prove something about an infinite data-structure, such as a stream or an infinite tree, but you would rather not subject yourself to coinduction. The unique fixed-point principle is an easyto- use, calculational alternative. The proof technique rests on the fact that certain recursion equations have unique solutions; if two elements of a coinductive type satisfy the same equation of this kind, then they are equal. In this paper we precisely characterize the conditions that gua...

Expand abstract
Publication status:
Published

Actions


Access Document


Publisher copy:
10.1145/2034574.2034821

Authors


James, DWH More by this author
Volume:
46
Issue:
9
Pages:
359-371
Publication date:
2011-09-05
DOI:
ISSN:
0362-1340
URN:
uuid:4f5ef44e-1c6c-4b2f-a77e-c2d8c019f13a
Source identifiers:
328771
Local pid:
pubs:328771
ISBN:
9781450308656

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP