1,722,467 research outputs found
Flexible coinductive logic programming
No full textRecursive 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
Enhancing Expressivity of Checked Corecursive Streams
No full textWe propose a novel approach to stream definition and manipulation. Our solution is based on two key ideas. Regular corecursion, which avoids non termination by detecting cyclic calls, is enhanced, by allowing in equations defining streams other operators besides the stream constructor. In this way, some non-regular streams are definable. Furthermore, execution includes a runtime check to ensure that the stream generated by a function call is well-defined, in the sense that access to an arbitrary index always succeeds. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme
Monadic Type-And-Effect Soundness
No full textWe introduce the abstract notions of monadic operational semantics, a small-step semantics where computational effects are modularly modeled by a monad, and type-and-effect system, including effect types whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usual in the non-monadic case, we can express progress and subject reduction, and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects, equipped with an expressive type-and-effect system We provide proofs of progress and subject reduction, parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies
An Effectful Object Calculus
No full textWe show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose,
and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative
of the last generation of OO languages, and the effectful extension is manageable enough for ordinary
programmers; notably, constructs to raise effects are just special methods. We equip the calculus
with an expressive type-and-effect system, which, again by relying on standard features such as
inheritance and generic types, allows a simple form of effect polymorphism. The soundness of
the type-and-effect system is expressed and proved by a recently introduced technique, where the
semantics is formalized by a one-step reduction relation from language expressions into monadic
ones, so that it is enough to prove progress and subject reduction properties on this relation
Equality of Corecursive Streams Defined by Finitary Equational Systems
No full textIn recent work, non-regular streams have been defined corecursively, by representing them with finitary equational systems built on top of various operators, besides the standard constructor. With finitary equational systems based only on the stream constructor, one can use the free theory of regular (a.k.a. rational) trees to get a sound and complete procedure to decide whether two streams are equal. However, this is not the case if one allows other operators in equations, since the underlying equational theory becomes non-trivial, hence equality of regular trees is too strong to guarantee termination of corecursive functions defined even only with the constructor and tail operators. To overcome this problem, we provide a weaker definition of equality between streams denoted by finitary equational systems built on different stream operators, including tail operator and constructor, and prove its soundness
An inductive abstract semantics for coFJ
No full textWe describe an inductive abstract semantics for coFJ, a Java-like calculus where, when the same method call is encountered twice, non-termination is avoided, and the programmer can decide the behaviour in this case, by writing a codefinition. The proposed semantics is abstract in the sense that evaluation is non-deterministic, and objects are possibly infinite. However, differently from typical coinductive handling of infinite values, the semantics is inductive, since it relies on detection of cyclic calls. Whereas soundness with respect to the reference coinductive semantics has already been proved, we conjecture that completeness with respect to the regular subset of such semantics holds as well. This relies on the fact that in the proposed semantics detection of cycles is non-deterministic, that is, does not necessarily happens the first time a cycle is found
Tracing and preventing sharing and mutation
No full textWe present a type and effect system for tracing and preventing sharing and mutation in imperative languages. That is, on one hand, the type system traces sharing possibly introduced by the evaluation of an expression, so that uniqueness and immutability properties can be easily detected. On the other hand, sharing and mutation can be prevented by type qualifiers which forbid some actions. Sharing is directly represented at the syntactic level as a relation among free variables, thanks to the fact that in the underlying calculus memory is encoded in terms
- …
