Related papers: The Recursion Theorem from a Different Angle
Obfuscation of computer programs has historically been approached either as a practical but \textit{ad hoc} craft to make reverse engineering subjectively difficult, or as a sound theoretical investigation unfortunately detached from the…
Proofs (sequent calculus, natural deduction) and imperative algorithms (pseudocodes) are two well-known coexisting concepts. Then what is their relationship? Our answer is that \[ imperative\ algorithms\ =\ proofs\ with\ cuts \] This…
The semantics of assignment and mutual exclusion in concurrent and multi-core/multi-processor systems is presented with attention to low level architectural features in an attempt to make the presentation realistic. Recursive functions on…
Can a problem undecidable with classical resources be decidable with quantum ones? The answer expected is no; as both being Turing theories, they should not solve the Halting problem - a problem unsolvable by any Turing machine. Yet, we…
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it…
This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one-- and two--sided bounds for such expectations, and show the…
We propose an operationally-based deductive proof method for program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LCTRSs) and the two programs as terms. The main feature of our…
We present a static analysis technique for non-termination inference of logic programs. Our framework relies on an extension of the subsumption test, where some specific argument positions can be instantiated while others are generalized.…
Time can be defined as the duration between events. It is irreversible. When used as a variable in quantifying the changing properties of matter, this irreversibility of time is incompatible with Newton's deterministic mechanics and with…
As a programming paradigm, answer set programming (ASP) brings about the usual issue of the human error. Hence, it is desirable to provide automated techniques that could help the programmer to find the error. This paper addresses the…
This paper considers the computational hardness of computing expected outcomes and deciding almost-sure termination of probabilistic programs. We show that deciding almost-sure termination and deciding whether the expected outcome of a…
This is the second installment to the project initiated in [Ma3]. In the first Part, I argued that both philosophy and technique of the perturbative renormalization in quantum field theory could be meaningfully transplanted to the theory of…
A problem is a multivalued function from a set of \emph{instances} to a set of \emph{solutions}. We consider only instances and solutions coded by sets of integers. A problem admits preservation of some computability-theoretic weakness…
We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is…
A Ramsey-like theorem is a statement of the form ``For every 2-coloring of $[\mathbb{N}]^2$, there exists an infinite set~$H \subseteq \mathbb{N}$ such that $[H]^2$ avoids some pattern''. We prove that none of these statements are…
The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present…
How to extract negative information from programs is an important issue in logic programming. Here we address the problem for functional logic programs, from a proof-theoretic perspective. The starting point of our work is CRWL (Constructor…
Probabilistic Logic Programming (PLP) languages, like ProbLog, naturally support reasoning under uncertainty, while maintaining a declarative and interpretable framework. Meanwhile, counterfactual reasoning (i.e., answering ``what if''…
We briefly describe -- mainly through very simple examples -- different kinds of answer-set programs with annotations that have been proposed for specifying: database repairs and consistent query answering; secrecy view and query evaluation…
The recent adoption of machine learning as a tool in real world decision making has spurred interest in understanding how these decisions are being made. Counterfactual Explanations are a popular interpretable machine learning technique…