334 research outputs found
Formal Languages, Formally and Coinductively
Full text linkTraditionally, formal languages are defined as sets of words. More
recently, the alternative coalgebraic or coinductive representation as
infinite tries, i.e., prefix trees branching over the alphabet, has
been used to obtain compact and elegant proofs of classic results in
language theory. In this paper, we study this representation in the
Isabelle proof assistant. We define regular operations on infinite
tries and prove the axioms of Kleene algebra for those
operations. Thereby, we exercise corecursion and coinduction and
confirm the coinductive view being profitable in formalizations, as it
improves over the set-of-words view with respect to proof automation
A Coalgebraic Decision Procedure for WS1S
Full text linkWeak monadic second-order logic of one successor (WS1S) is a simple and natural formalism to specify regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e. they escape the simple and natural formalism by translating formulas into equally expressive regular structures such as finite automata, regular expressions, or games. In this work, we devise a coalgebraic decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle
Generic Authenticated Data Structures, Formally
Full text linkAuthenticated data structures are a technique for outsourcing data storage and maintenance to an untrusted server. The server is required to produce an efficiently checkable and cryptographically secure proof that it carried out precisely the requested computation. Recently, Miller et al. [https://doi.org/10.1145/2535838.2535851] demonstrated how to support a wide range of such data structures by integrating an authentication construct as a first class citizen in a functional programming language. In this paper, we put this work to the test of formalization in the Isabelle proof assistant. With Isabelle’s help, we uncover and repair several mistakes and modify the small-step semantics to perform call-by-value evaluation rather than requiring terms to be in administrative normal form
Quotients of Bounded Natural Functors
Full text linkThe functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and—under certain conditions—subtypes are known to preserve the BNF structure. In this article, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. Surprisingly, lifting the structure in the obvious manner fails for some quotients, a problem that also affects the quotients of polynomial functors used in the Lean proof assistant. We provide a strictly more general lifting scheme that supports such problematic quotients. We extend the Isabelle/HOL proof assistant with a command that automates the registration of a quotient type as a BNF, reducing the proof burden on the user from the full set of BNF axioms to our inheritance conditions. We demonstrate the command’s usefulness through several case studies.</p
Efficient Evaluation of Arbitrary Relational Calculus Queries
Full text linkThe relational calculus (RC) is a concise, declarative query language.
However, existing RC query evaluation approaches are inefficient and often
deviate from established algorithms based on finite tables used in database
management systems. We devise a new translation of an arbitrary RC query into
two safe-range queries, for which the finiteness of the query's evaluation
result is guaranteed. Assuming an infinite domain, the two queries have the
following meaning: The first is closed and characterizes the original query's
relative safety, i.e., whether given a fixed database, the original query
evaluates to a finite relation. The second safe-range query is equivalent to
the original query, if the latter is relatively safe. We compose our
translation with other, more standard ones to ultimately obtain two SQL
queries. This allows us to use standard database management systems to evaluate
arbitrary RC queries. We show that our translation improves the time complexity
over existing approaches, which we also empirically confirm in both realistic
and synthetic experiments
From Nondeterministic to Multi-Head Deterministic Finite-State Transducers (Track B: Automata, Logic, Semantics, and Theory of Programming)
Full text linkEvery nondeterministic finite-state automaton is equivalent to a deterministic finite-state automaton. This result does not extend to finite-state transducers - finite-state automata equipped with a one-way output tape. There is a strict hierarchy of functions accepted by one-way deterministic finite-state transducers (1DFTs), one-way nondeterministic finite-state transducers (1NFTs), and two-way nondeterministic finite-state transducers (2NFTs), whereas the two-way deterministic finite-state transducers (2DFTs) accept the same family of functions as their nondeterministic counterparts (2NFTs).
We define multi-head one-way deterministic finite-state transducers (mh-1DFTs) as a natural extension of 1DFTs. These transducers have multiple one-way reading heads that move asynchronously over the input word. Our main result is that mh-1DFTs can deterministically express any function defined by a one-way nondeterministic finite-state transducer. Of independent interest, we formulate the all-suffix regular matching problem, which is the problem of deciding for each suffix of an input word whether it belongs to a regular language. As part of our proof, we show that an mh-1DFT can solve all-suffix regular matching, which has applications, e.g., in runtime verification
Electronic spectroscopy of carbon chain radicals using cw cavity ring down in conjunction with mass detection
Full text linkThe electronic absorption spectrum of the 2A'' − X 2A'' origin band of the
nonlinear carbon chain radical C6H4
+ was rotationally resolved by cw-CRD
spectroscopy [41]. It was analysed using a least-squares method and the rotational
constants of the ground and excited states were determined accurately. The 581 nm
band observed under the same discharge conditions is assigned to the same electronic
transition of C6H4
+ but involving the excitation of the ν12 vibrational mode in the
upper state based on comparison with ab initio results. The presented data provide a
basis for future observations of the C6H4
+ radical in both millimeter and infrared
regions.
A linear time-of-flight mass spectrometer was constructed to provide on-line
monitoring of the plasma discharge with a mass resolution of 1 amu at a range up to
120 amu. The results from the acetylene/helium plasma discharge are in good
agreement with those obtained using the reflectron TOF mass spectrometer and a
similar ion source [42]. To improve the experimental set-up, the following
modifications can be made:
• Transferring the signal from the oscilloscope directly to a PC via a
GPIB card will increase the speed of data processing;
• Computer control of the voltage applied will make the spectrometer
easier to operate;
• Using a metal grid at ground potential in front of MCP detector will
increase the flight time of ions improving the mass resolution;
• Installing a focusing lens will increase the number of ions arriving at
the detector, and therefore increase the signal on the oscilloscope
Bindings as Bounded Natural Functors
Full text linkInternational audiencethe Romanian Academy, Romania DMITRIY TRAYTEL, ETH Zürich, Switzerland We present a general framework for specifying and reasoning about syntax with bindings. Abstract binder types are modeled using a universe of functors on sets, subject to a number of operations that can be used to construct complex binding patterns and binding-aware datatypes, including non-well-founded and infinitely branching types, in a modular fashion. Despite not committing to any syntactic format, the framework is "concrete" enough to provide definitions of the fundamental operators on terms (free variables, alpha-equivalence, and capture-avoiding substitution) and reasoning and definition principles. This work is compatible with classical higher-order logic and has been formalized in the proof assistant Isabelle/HOL
Practical Relational Calculus Query Evaluation
Full text linkThe relational calculus (RC) is a concise, declarative query language. However, existing RC query evaluation approaches are inefficient and often deviate from established algorithms based on finite tables used in database management systems. We devise a new translation of an arbitrary RC query into two safe-range queries, for which the finiteness of the query’s evaluation result is guaranteed. Assuming an infinite domain, the two queries have the following meaning: The first is closed and characterizes the original query’s relative safety, i.e., whether given a fixed database, the original query evaluates to a finite relation. The second safe-range query is equivalent to the original query, if the latter is relatively safe. We compose our translation with other, more standard ones to ultimately obtain two SQL queries. This allows us to use standard database management systems to evaluate arbitrary RC queries. We show that our translation improves the time complexity over existing approaches, which we also empirically confirm in both realistic and synthetic experiments
Verified Progress Tracking for Timely Dataflow
Full text linkLarge-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data- and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We modeled the progress tracking protocol as a combination of two independent transition systems in the Isabelle/HOL proof assistant. We specified and verified the safety of the two components and of the combined protocol. To this end, we identified abstract assumptions on dataflow programs that are sufficient for safety and were not previously formalized
- …
