اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn Word and Frontier Languages of Unsafe Higher-Order Grammars
362
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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, concatenatio
n 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.
Context-Free Grammars (CFGs) and Parsing Expression Grammars (PEGs) have several similarities and a few differences in both their syntax and semantics, but they are usually presented through formalisms that hinder a proper comparison. In this paper w
e present a new formalism for CFGs that highlights the similarities and differences between them. The new formalism borrows from PEGs the use of parsing expressions and the recognition-based semantics. We show how one way of removing non-determinism from this formalism yields a formalism with the semantics of PEGs. We also prove, based on these new formalisms, how LL(1) grammars define the same language whether interpreted as CFGs or as PEGs, and also show how strong-LL(k), right-linear, and LL-regular grammars have simple language-preserving translations from CFGs to PEGs.
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 kno
wn 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.
We study the computational complexity of universality and inclusion problems for unambiguous finite automata and context-free grammars. We observe that several such problems can be reduced to the universality problem for unambiguous context-free gram
mars. The latter problem has long been known to be decidable and we propose a PSPACE algorithm that works by reduction to the zeroness problem of recurrence equations with convolution. We are not aware of any non-trivial complexity lower bounds. However, we show that computing the coin-flip measure of an unambiguous context-free language, a quantitative generalisation of universality, is hard for the long-standing open problem SQRTSUM.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
