Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCertified Context-Free Parsing: A formalisation of Valiants Algorithm in Agda
62
0
0.0
(
0
)
Added by
J\\\"urgen Koslowski
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Valiant (1975) has developed an algorithm for recognition of context free languages. As of today, it remains the algorithm with the best asymptotic complexity for this purpose. In this paper, we present an algebraic specification, implementation, and proof of correctness of a generalisation of Valiants algorithm. The generalisation can be used for recognition, parsing or generic calculation of the transitive closure of upper triangular matrices. The proof is certified by the Agda proof assistant. The certification is representative of state-of-the-art methods for specification and proofs in proof assistants based on type-theory. As such, this paper can be read as a tutorial for the Agda system.
rate research
Read More
We describe an extension of Earleys parser for stochastic context-free grammars that computes the following quantities given a stochastic context-free grammar and an input string: a) probabilities of successive prefixes being generated by the grammar; b) probabilities of substrings being generated by the nonterminals, including the entire string being generated by the grammar; c) most likely (Viterbi) parse of the string; d) posterior expected number of applications of each grammar production, as required for reestimating rule probabilities. (a) and (b) are computed incrementally in a single left-to-right pass over the input. Our algorithm compares favorably to standard bottom-up parsing methods for SCFGs in that it works efficiently on sparse grammars by making use of Earleys top-down control structure. It can process any context-free rule format without conversion to some normal form, and combines computations for (a) through (d) in a single algorithm. Finally, the algorithm has simple extensions for processing partially bracketed inputs, and for finding partial parses and their likelihoods on ungrammatical inputs.
We survey recent results on the topological complexity of context-free omega-languages which form the second level of the Chomsky hierarchy of languages of infinite words. In particular, we consider the Borel hierarchy and the Wadge hierarchy of non-deterministic or deterministic context-free omega-languages. We study also decision problems, the links with the notions of ambiguity and of degrees of ambiguity, and the special case of omega-powers.
We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Buchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We show also that the determinacy of Wadge games between two players in charge of omega-languages accepted by 1-counter Buchi automata is equivalent to the (effective) analytic Wadge determinacy. Using some results of set theory we prove that one can effectively construct a 1-counter Buchi automaton A and a Buchi automaton B such that: (1) There exists a model of ZFC in which Player 2 has a winning strategy in the Wadge game W(L(A), L(B)); (2) There exists a model of ZFC in which the Wadge game W(L(A), L(B)) is not determined. Moreover these are the only two possibilities, i.e. there are no models of ZFC in which Player 1 has a winning strategy in the Wadge game W(L(A), L(B)).
The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and context-free properties by ensuring decidability and tractability in the combined setting. To this end we introduce two real-time linear temporal logics for specifying quantitative timing context-free requirements in a pointwise semantics setting: Event-Clock Nested Temporal Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). The logic EC_NTL is an extension of both the logic CaRet (a context-free extension of standard LTL) and Event-Clock Temporal Logic (a tractable real-time logical framework related to the class of Event-Clock automata). We prove that satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Automata (VPTA) against EC_NTL are decidable and EXPTIME-complete. The other proposed logic NMTL is a context-free extension of standard Metric Temporal Logic (MTL). It is well known that satisfiability of future MTL is undecidable when interpreted over infinite timed words but decidable over finite timed words. On the other hand, we show that by augmenting future MTL with future context-free temporal operators, the satisfiability problem turns out to be undecidable also for finite timed words. On the positive side, we devise a meaningful and decidable fragment of the logic NMTL which is expressively equivalent to EC_NTL and for which satisfiability and visibly model-checking of VPTA are EXPTIME-complete.
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a compound value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the untyped version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
