Coinduction Plain and Simple
Coinduction refers to both a technique for the definition of infinite streams, so-called codata, and a technique for proving the equality of coinductively specified codata. This article first reviews coinduction in declarative programming. Second, it reviews and slightly extends the formalism commonly used for specifying codata. Third, it generalizes the coinduction proof principle, which has been originally specified for the equality predicate only, to other predicates. This generalization makes the coinduction proof principle more intuitive and stresses its closeness with structural induction. The article finally suggests in its conclusion extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Towards Coinductive Models for Natural Language Understanding. Bringing together Deep Learning and Deep Semantics
This article contains a proposal to add coinduction to the computational apparatus of natural language understanding. This, we argue, will provide a basis for more realistic, computationally sound, and scalable models of…
Machine TranslationNatural Language UnderstandingTowards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of (possibly irregular) infinite data. Both instances of coinductive rea…
PositionUniversal Reinforcement Learning in Coalgebras: Asynchronous Stochastic Computation via Conduction
In this paper, we introduce a categorial generalization of RL, termed universal reinforcement learning (URL), building on powerful mathematical abstractions from the study of coinduction on non-well-founded sets and univ…
Reinforcement LearningCertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learning in safety-critical settings inspires …
Decision Makingreinforcement-learningReinforcement LearningReinforcement Learning (RL)+1Distill n' Explain: explaining graph neural networks using simple surrogates
Explaining node predictions in graph neural networks (GNNs) often boils down to finding graph substructures that preserve predictions. Finding these structures usually implies back-propagating through the GNN, bonding th…
Knowledge Distillation