Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userNon-Deterministic Functions as Non-Deterministic Processes (Extended Version)
64
0
0.0
(
0
)
Added by
Jorge A. P\\'erez
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambdafail via typed processes in spi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.
rate research
Read More
We show that there are $Sigma_3^0$-complete languages of infinite words accepted by non-deterministic Petri nets with Buchi acceptance condition, or equivalently by Buchi blind counter automata. This shows that omega-languages accepted by non-deterministic Petri nets are topologically more complex than those accepted by deterministic Petri nets.
In this paper, we show that every D3-directing CNFA can be mapped uniquely to a DFA with the same synchronizing word length. This implies that v{C}ernys conjecture generalizes to CNFAs and that the general upper bound for the length of a shortest D3-directing word is equal to the Pin-Frankl bound for DFAs. As a second consequence, for several classes of CNFAs sharper bounds are established. Finally, our results allow us to detect all critical CNFAs on at most 6 states. It turns out that only very few critical CNFAs exist.
We study a variant of the Ackermann encoding $mathbb{N}(x) := sum_{yin x}2^{mathbb{N}(y)}$ of the hereditarily finite sets by the natural numbers, applicable to the larger collection $mathsf{HF}^{1/2}$ of the hereditarily finite hypersets. The proposed variation is obtained by simply placing a `minus sign before each exponent in the definition of $mathbb{N}$, resulting in the expression $mathbb{R}(x) := sum_{yin x}2^{-mathbb{R}(y)}$. By a careful analysis, we prove that the encoding $mathbb{R}_{A}$ is well-defined over the whole collection $mathsf{HF}^{1/2}$, as it allows one to univocally assign a real-valued code to each hereditarily finite hyperset. We also address some preliminary cases of the injectivity problem for $mathbb{R}_{A}$.
We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. The first approach eliminates non-determinism by considering the set of all non-deterministic values produced by an application. The second approach encodes every non-deterministic choice that the application could perform. We consider our initial experiment a success. Although proving properties of programs is a notoriously difficult task, the functional logic paradigm does not seem to add any significant layer of difficulty or complexity to the task.
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Buchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, enquote{Safraless} LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
