Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCoaxioms: flexible coinductive definitions by inference systems
77
0
0.0
(
0
)
Added by
Thorsten Wissmann
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Authors
Francesco Dagnino
Ask ChatGPT about the research
No Arabic abstract
We introduce a generalized notion of inference system to support more flexible interpretations of recursive definitions. Besides axioms and inference rules with the usual meaning, we allow also coaxioms, which are, intuitively, axioms which can only be applied at infinite depth in a proof tree. Coaxioms allow us to interpret recursive definitions as fixed points which are not necessarily the least, nor the greatest one, whose existence is guaranteed by a smooth extension of classical results. This notion nicely subsumes standard inference systems and their inductive and coinductive interpretation, thus allowing formal reasoning in cases where the inductive and coinductive interpretation do not provide the intended meaning, but are rather mixed together.
rate research
Read More
After surveying classical results, we introduce a generalized notion of inference system to support structural recursion on non-well-founded data types. Besides axioms and inference rules with the usual meaning, a generalized inference system allows coaxioms, which are, intuitively, axioms which can only be applied at infinite depth in a proof tree. This notion nicely subsumes standard inference systems and their inductive and coinductive interpretation, while providing more flexibility. Indeed, the classical results can be extended to our generalized framework, interpreting recursive definitions as fixed points which are not necessarily the least, nor the greatest one. This allows formal reasoning in cases where the inductive and coinductive interpretation do not provide the intended meaning, or are mixed together.
We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of gDTT are novel type and term formers involving what we call `delayed substitutions. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model.
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Lob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Ruttens behavioural differential equations.
Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by coclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels. This paper is under consideration for acceptance in TPLP.
This note formally defines the concept of coinductive validity of judgements, and contrasts it with inductive validity. For both notions it shows how a judgement is valid iff it has a formal proof. Finally, it defines and illustrates the notion of a proof by coinduction.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
