Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userHigher-Order Operator Precedence Languages
161
0
0.0
(
0
)
Added by
EPTCS
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Floyds Operator Precedence (OP) languages are a deterministic context-free family having many desirable properties. They are locally and parallely parsable, and languages having a compatible structure are closed under Boolean operations, concatenation and star; they properly include the family of Visibly Pushdown (or Input Driven) languages. OP languages are based on three relations between any two consecutive terminal symbols, which assign syntax structure to words. We extend such relations to k-tuples of consecutive terminal symbols, by using the model of strictly locally testable regular languages of order k at least 3. The new corresponding class of Higher-order Operator Precedence languages (HOP) properly includes the OP languages, and it is still included in the deterministic (also in reverse) context free family. We prove Boolean closure for each subfamily of structurally compatible HOP languages. In each subfamily, the top language is called max-language. We show that such languages are defined by a simple cancellation rule and we prove several properties, in particular that max-languages make an infinite hierarchy ordered by parameter k. HOP languages are a candidate for replacing OP languages in the various applications where they have have been successful though sometimes too restrictive.
rate research
Read More
Higher-order grammars are extensions of regular and context-free grammars, where non-terminals may take parameters. They have been extensively studied in 1980s, and restudied recently in the context of model checking and program verification. We show that the class of unsafe order-(n+1) word languages coincides with the class of frontier languages of unsafe order-n tree languages. We use intersection types for transforming an order-(n+1) word grammar to a corresponding order-n tree grammar. The result has been proved for safe languages by Damm in 1982, but it has been open for unsafe languages, to our knowledge. Various known results on higher-order grammars can be obtained as almost immediate corollaries of our result.
In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and vario
In a previous work we introduced slice graphs as a way to specify both infinite languages of directed acyclic graphs (DAGs) and infinite languages of partial orders. Therein we focused on the study of Hasse diagram generators, i.e., slice graphs that generate only transitive reduced DAGs, and showed that they could be used to solve several problems related to the partial order behavior of p/t-nets. In the present work we show that both slice graphs and Hasse diagram generators are worth studying on their own. First, we prove that any slice graph SG can be effectively transformed into a Hasse diagram generator HG representing the same set of partial orders. Thus from an algorithmic standpoint we introduce a method of transitive reducing infinite families of DAGs specified by slice graphs. Second, we identify the class of saturated slice graphs. By using our transitive reduction algorithm, we prove that the class of partial order languages representable by saturated slice graphs is closed under union, intersection and even under a suitable notion of complementation (cut-width complementation). Furthermore partial order languages belonging to this class can be tested for inclusion and admit canonical representatives in terms of Hasse diagram generators. As an application of our results, we give stronger forms of some results in our previous work, and establish some unknown connections between the partial order behavior of $p/t$-nets and other well known formalisms for the specification of infinite families of partial orders, such as Mazurkiewicz trace languages and message sequence chart (MSC) languages.
Higher-order constrained Horn clauses (HoCHC) are a semantically-invariant system of higher-order logic modulo theories. With semi-decidable unsolvability over a semi-decidable background theory, HoCHC is suitable for safety verification. Less is known about its relation to larger classes of higher-order verification problems. Motivated by program equivalence, we introduce a coinductive version of HoCHC that enjoys a greatest model property. We define an encoding of higher-order recursion schemes (HoRS) into HoCHC logic programs. Correctness of this encoding reduces decidability of the open HoRS equivalence problem -- and, thus, the LambdaY-calculus Bohm tree equivalence problem -- to semi-decidability of coinductive HoCHC over a complete and decidable theory of trees.
Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. We show that the game semantics of any FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation. Moreover, we identify a fragment of FICA that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
