文章基本信息

标题：Flexible Coinduction in Agda
本地全文：下载
作者：Ciccone, Luca ; Dagnino, Francesco ; Zucca, Elena 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：193
页码：13:1-13:19
DOI：10.4230/LIPIcs.ITP.2021.13
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We provide an Agda library for inference systems, also supporting their recent generalization allowing flexible coinduction, that is, interpretations which are neither inductive, nor purely coinductive. A specific inference system can be obtained as an instance by writing a set of meta-rules, in an Agda format which closely resembles the usual one. In this way, the user gets for free the related properties, notably the inductive and coinductive intepretation and the corresponding proof principles. Moreover, a significant modularity is achieved. Indeed, rather than being defined from scratch and with a built-in interpretation, an inference system can also be obtained by composition operators, such as union and restriction to a smaller universe, and its semantics can be modularly chosen as well. In particular, flexible coinduction is obtained by composing in a certain way the interpretations of two inference systems. We illustrate the use of the library by several examples. The most significant one is a big-step semantics for the Î»-calculus, where flexible coinduction allows to obtain a special result (â^Z) for all and only the diverging computations, and the proof of equivalence with small-step semantics is carried out by relying on the proof principles offered by the library.
关键词：inference systems; induction; coinduction