Wyniki wyszukiwania - BazTech

Ograniczanie wyników

4 Fundamenta Informaticae

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: coinduction

Sortuj według:

Ogranicz wyniki do:

Coinductive Algorithms for Büchi Automata

Kuperberg Denis, Pinault Laureline, Pous Damien

Fundamenta Informaticae

2021

Vol. 180, nr 4

351--373

We propose a new algorithm for checking language equivalence of non-deterministic Büchi automata. We start from a construction proposed by Calbrix, Nivat and Podelski, which makes it possible to reduce the problem to that of checking equivalence of automata on finite words. Although this construction generates large and highly non-deterministic automata, we show how to exploit their specific structure and apply state-of-the art techniques based on coinduction to reduce the state-space that has to be explored. Doing so, we obtain algorithms which do not require full determinisation or complementation.

Decidability of Several Concepts of Finiteness for Simple Types

Santo José Espírito, Matthes Ralph, Pinto Luís

Fundamenta Informaticae

2019

Vol. 170, nr 1-3

111--138

If we consider as “member” of a simple type the outcome of any successful (possibly infinite) run of bottom-up proof search that starts from the type, then several concepts of “finiteness” for simple types are possible: the finiteness of the search space, the finiteness of any member, or the finiteness of the number of finite members (in other words, the inhabitants). In this paper we show that these three concepts are instances of the same parameterized notion of finiteness, and that a single, parameterized proof shows the decidability of all of them. One instance of this result means that termination of proof search is decidable. A separate result is that emptiness is also decidable (where emptiness is absence of “members” as above, not just absence of inhabitants). This fact is an ingredient of the main decidability result, but it also has a different application, the definition of the pruned search space - the one where branches leading to failure are chopped off. We conclude with our version of König’s lemma for simple types: a simple type has an infinite member exactly when the pruned search space is infinite.

A Theoretical Perspective of Coinductive Logic Programming

Ancona D., Dovier A.

Fundamenta Informaticae

2015

Vol. 140, nr 3/4

221--246

In this paper we study the semantics of Coinductive Logic Programming and clarify its intrinsic computational limits, which prevent, in particular, the definition of a complete, computable, operational semantics. We propose a new operational semantics that allows a simple correctness result and the definition of a simple meta-interpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

Coinductive axiomatization of recursive type equality and subtyping

Brandt M., Henglein F.

Fundamenta Informaticae

1998

Vol. 33, nr 4

309-338

We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle). It states that from A,Pý P one may deduce Aý P, where P is either a type equality t = t1 or type containment t