A restricted computation model on Scott domains and its partial primitive recursive functionals

1998 ◽  
Vol 37 (7) ◽  
pp. 443-481 ◽  
Author(s):  
Karl-Heinz Niggl
Keyword(s):  
Computation Model ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice

2019 ◽  
Vol 29 (4) ◽  
pp. 519-554 ◽  
Author(s):  
Thomas Powell
Keyword(s):  
Large Family ◽  
Classical Analysis ◽  
Wide Range ◽  
Simple Corollary ◽  
The Many ◽  
Primitive Recursive ◽  
Dependent Choice ◽  
Primitive Recursive Functionals ◽  
Negative Translation

Abstract During the last 20 years or so, a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work, we present the many variants of bar recursion used in this context as instantiations of a parametrized form of backward recursion, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrized dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi–Bezem–Coquand functional, modified realizability and the more recent products of selection functions of Escardó and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.

On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising

1982 ◽  
Vol 47 (2) ◽  
pp. 395-402 ◽  
Author(s):  
Jan Terlouw
Keyword(s):  
Lower Order ◽  
Recursive Function ◽  
Functional Interpretation ◽  
Crucial Step ◽  
Recursive Functions ◽  
Order Types ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

It is known that every < ε0-recursive function is also a primitive recursive functional. Kreisel has proved this by means of Gödel's functional-interpretation, using that every < ε0-recursive function is provably recursive in Heyting's arithmetic [2, §3.4]. Parsons obtained a refinement of Kreisel's result by a further examination of Gödel's interpretation with regard to type levels [3, Theorem 5], [4, §4]. A quite different proof is provided by the research into extensions of the Grzegorczyk hierarchy as done by Schwichtenberg and Wainer: this yields another characterization of the < ε0-recursive functions from which easily appears that these are primitive recursive functionals (see [5] in combination with [6, Chapter II]).However, these proofs are indirect and do not show how, in general, given a definition tree of an ordinal recursive functional, transfinite recursions can be replaced (in a straightforward way) by recursions over wellorderings of lower order types. The argument given by Tait in [9, pp. 189–191] seems to be an improvement in this respect, but the crucial step in it is (at least in my opinion) not very clear.

A system of abstract constructive ordinals

1972 ◽  
Vol 37 (2) ◽  
pp. 355-374 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Finite Type ◽  
Free Variable ◽  
Transfinite Induction ◽  
Functional Interpretation ◽  
Variable Theory ◽  
Inductive Definitions ◽  
Heyting Arithmetic ◽  
Abstract Notion ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

As Gödel [6] has pointed out, there is a certain interchangeability between the intuitionistic notion of proof and the notion of constructive functional of finite type. He achieves this interchange in the direction from logic to functionals by his functional interpretation of Heyting arithmetic H in a free variable theory T of primitive recursive functionals of finite type. In the present paper we shall extend Gödel's functional interpretation to the case in which H and T are extended by adding an abstract notion of constructive ordinal. In other words, we obtain the Gödel functional interpretation of an intuitionistic theory U of numbers (i.e., nonnegative integers) and constructive ordinals in a free variable theory V of finite type over both numbers and constructive ordinals. This allows us to obtain an analysis of noniterated positive inductive definitions [8].The notion of constructive ordinal to be treated is as follows. There is given a function J which embeds the nonnegative integers in the constructive ordinals. A constructive ordinal of the form Jn is said to be minimal. There is also given a function δ which associates to each constructive ordinal Z and number n a constructive ordinal δZn which we denote by Zn. When Z is nonminimal, each Zn is called an immediate predecessor of Z. The basic principle for forming constructive ordinals says: for every function f from numbers n to constructive ordinals, there exists a constructive ordinal Z such that Zn = fn for all n. The principle of transfinite induction with respect to constructive ordinals says: if a property Q(Z) of constructive ordinals Z holds for minimal Z, and if ∀nQ(Zn) → Q(Z) holds for all Z, then Q(Z) holds for all Z.

Ordinal analysis of terms of finite type

1980 ◽  
Vol 45 (3) ◽  
pp. 493-504 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Finite Type ◽  
Axiom Of Choice ◽  
Transfinite Induction ◽  
Critical Number ◽  
Ordinal Analysis ◽  
Primitive Recursion ◽  
Successor Relation ◽  
Ordinal Notations ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

Sanchis [Sa] and Diller [Di] have introduced an interesting relation between terms for primitive recursive functionals of finite type in order to obtain a computability proof. The method is as follows. First the relation is shown to be well-founded. Then computability of each term is obtained by transfinite induction over the relation.Their relation is given by various clauses which define the (immediate) successors of a term. Hence, starting with a term H and repeatedly applying the successor relation one generates the tree of H (say). The problem is to prove that the trees are well-founded. In their proofs Sanchis and Diller use the axiom of bar induction. Diller also gives a proof using transfinite induction: each tree is shown to have a length b < φω(0) (the first ω-critical number) and the induction is over ordinals less than or equal to b.For proof-theoretic purposes it would be desirable to employ a method of proof which is more elementary than the axiom of bar induction and also to obtain a smaller ordinal bound. The purpose of the following is to provide such a method. We show that for a primitive recursive term H of finite type the tree generated by the relation of Sanchis and Diller has length less than ε0. Our method is similar to that used by Tait [Ta] in his theory of infinite terms. The immediately natural metamathematics is elementary intuitionistic analysis with the axiom of choice and transfinite induction over the relevant ordinal notations. We give several versions of the basic list of successor clauses, and for one version we show how to carry out the treatment in Skolem arithmetic (with primitive recursion of lowest type).

scholarly journals Towards efficient verification of population protocols

2021 ◽  
Author(s):  
Michael Blondin ◽  
Javier Esparza ◽  
Stefan Jaax ◽  
Philipp J. Meyer
Keyword(s):  
Linear Constraints ◽  
Computational Power ◽  
High Complexity ◽  
Reachability Problem ◽  
Population Protocols ◽  
Finite State ◽  
State Agents ◽  
Efficient Verification ◽  
Primitive Recursive ◽  
Very High

AbstractPopulation protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is -hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class $${ WS}^3$$ WS 3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that $${ WS}^3$$ WS 3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership and correctness problems for $${ WS}^3$$ WS 3 reduce to solving boolean combinations of linear constraints over $${\mathbb {N}}$$ N . This allowed us to develop the first software able to automatically prove correctness for all of the infinitely many possible inputs.

Sign in / Sign up

Export Citation Format

Share Document