Reseña: Recursive functions on lazy lists via domains and topologies

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL Recursive functions on lazy lists via domains and topologies.

Sus autores son

• Andreas Lochbihler (del Institute of Information Security, ETH Zurich) y
• Johannes Hölzl (del Institut für Informatik, TU Müunchen).

Su resumen es

The usual definition facilities in theorem provers cannot handle all recursive functions on codatatypes; the filter function on lazy lists is a prime counterexample. We present two new ways of directly defining functions like filter by exploiting their dual nature as producers and consumers. Borrowing from domain theory and topology, we define them as a least fixpoint (producer view) and as a continuous extension (consumer view). Both constructions yield proof principles that allow elegant proofs.

El trabajo se presentará el lune 14 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).