1,943,028 research outputs found
Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered
No full textAsada and Kobayashi [ICALP 2017] conjectured a higher-order version of Kruskal's tree theorem, and proved a pumping lemma for higher-order languages modulo the conjecture. The conjecture has been proved up to order-2, which implies that Asada and Kobayashi's pumping lemma holds for order-2 tree languages, but remains open for order-3 or higher. In this paper, we prove a variation of the conjecture for order-3. This is sufficient for proving that a variation of the pumping lemma holds for order-3 tree languages (equivalently, for order-4 word languages)
Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
No full textHigher-order grammars have recently been studied actively in the context of automated verification of higher-order programs. Asada and Kobayashi have previously shown that, for any order-(n+1) word grammar, there exists an order-n grammar whose frontier language coincides with the language generated by the word grammar. Their translation, however, blows up the size of the grammar, which inhibited complexity-preserving reductions from decision problems on word grammars to those on tree grammars. In this paper, we present a new translation from order-(n+1) word grammars to order-n tree grammars that is size-preserving in the sense that the size of the output tree grammar is polynomial in the size of an input tree grammar. The new translation and its correctness proof are arguably much simpler than the previous translation and proof
LIPIcs, Volume 195, FSCD 2021, Complete Volume
No full textLIPIcs, Volume 195, FSCD 2021, Complete Volum
Front Matter, Table of Contents, Preface, Conference Organization
No full textFront Matter, Table of Contents, Preface, Conference Organizatio
A Cyclic Proof System for HFL_ℕ
No full textA cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFL_ℕ, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.’s recent work on reductions from program verification to HFL_ℕ validity checking
Kobayashi, Noboru -- 1986 -- Correspondence, Individual -- letter, 1986-11-17
No full textLetter from Kobayashi, Noboru to Sabin, Albert B. dated 1986-11-17.Sabin Collection Fair Use Policy</a
A Probabilistic Higher-Order Fixpoint Logic
No full textWe introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the μ^p-calculus. We show that PHFL is strictly more expressive than the μ^p-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the μ-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky’s μ-arithmetic to PHFL, which implies that PHFL model checking is Π^1₁-hard and Σ^1₁-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system
Passport of Moto Shigeta Kobayashi
No full textPhotograph shows the front side of the 1913 Japanese passport issued to Moto Kobayashi, "picture bride" of Mitsutaro Kobayashi, a farmer in Harris County, Texas
On Word and Frontier Languages of Unsafe Higher-Order Grammars
No full textHigher-order grammars are an extension of regular and context-free grammars, where nonterminals may take parameters. They have been extensively studied in 1980's, 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
Pumping Lemma for Higher-order Languages
No full textWe study a pumping lemma for the word/tree languages generated by higher-order grammars. Pumping lemmas are known up to order-2 word languages (i.e., for regular/context-free/indexed languages), and have been used to show that a given language does not belong to the classes of regular/context-free/indexed languages. We prove a pumping lemma for word/tree languages of arbitrary orders, modulo a conjecture that a higher-order version of Kruskal's tree theorem holds. We also show that the conjecture indeed holds for the order-2 case, which yields a pumping lemma for order-2 tree languages and order-3 word languages
- …
