اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA Rice-like theorem for primitive recursive functions
47
0
0.0
(
0
)
تأليف
Mathieu Hoyrup
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We provide an explicit characterization of the properties of primitive recursive functions that are decidable or semi-decidable, given a primitive recursive index for the function. The result is much more general as it applies to any c.e. class of total computable functions. This is an analog of Rice and Rice-Shapiro theorem, for restricted classes of total computable functions.
قيم البحث
اقرأ أيضاً
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursi
on will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum programs. This logic is an extension of quantum Hoare logic for quantum While-programs. The (relative) completeness of the logic is proved, and its effectiveness is shown by a running example: fixed-point Grovers search.
We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula equations. We state and prove a fixed-point theorem for Horn formula equ
ations which is based on expressing the fixed-point computation of a minimal model of a set of Horn clauses on the object level as a formula in first-order logic with a least fixed point operator. We describe several corollaries of this fixed-point theorem, in particular concerning the logical foundations of program verification, and sketch how to generalise it to incorporate abstract interpretations.
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursi
on will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grovers search, and recursive quantum Fourier sampling.
This paper proposes a recursive diffeomorphism based regression method for one-dimensional generalized mode decomposition problem that aims at extracting generalized modes $alpha_k(t)s_k(2pi N_kphi_k(t))$ from their superposition $sum_{k=1}^K alpha_k
(t)s_k(2pi N_kphi_k(t))$. First, a one-dimensional synchrosqueezed transform is applied to estimate instantaneous information, e.g., $alpha_k(t)$ and $N_kphi_k(t)$. Second, a novel approach based on diffeomorphisms and nonparametric regression is proposed to estimate wave shape functions $s_k(t)$. These two methods lead to a framework for the generalized mode decomposition problem under a weak well-separation condition. Numerical examples of synthetic and real data are provided to demonstrate the fruitful applications of these methods.
In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity
bounds for the respective logics. We also present CondLean, a theorem prover for these logics implementing SeqS calculi written in SICStus Prolog.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
