scholarly journals Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

2011 ◽  
Author(s):  
Diego Figueira ◽  
Santiago Figueira ◽  
Sylvain Schmitz ◽  
Philippe Schnoebelen
Keyword(s):  
Primitive Recursive ◽  
Dickson's Lemma ◽  
Dickson’S Lemma

scholarly journals Dickson’s lemma and weak Ramsey theory

2018 ◽  
Vol 58 (3-4) ◽  
pp. 413-425
Author(s):  
Yasuhiko Omata ◽  
Florian Pelupessy
Keyword(s):  
Ramsey Theory ◽  
Dickson's Lemma ◽  
Dickson’S Lemma

A Proof of Parikh’s Theorem via Dickson’s Lemma

2021 ◽  
Vol 32 (02) ◽  
pp. 163-173
Author(s):  
Toshihiro Koga
Keyword(s):  
Tree Decomposition ◽  
Clear Separation ◽  
Context Free ◽  
Dickson's Lemma ◽  
Dickson’S Lemma ◽  
Context Free Grammars

In this paper, we give a proof of Parikh’s semilinear theorem via Dickson’s lemma. It is notable that our proof provides a clear separation between properties derived from Dickson’s lemma and tree decomposition for context-free grammars.

scholarly journals A Formal Proof of Dickson’s Lemma in ACL2

2003 ◽  
pp. 49-58 ◽  
Author(s):  
F. J. Martın-Mateos ◽  
J. A. Alonso ◽  
M. J. Hidalgo ◽  
J. L. Ruiz-Reina
Keyword(s):  
Formal Proof ◽  
Dickson's Lemma ◽  
Dickson’S Lemma

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.

Simplifications of the recursion scheme

1971 ◽  
Vol 36 (4) ◽  
pp. 653-665 ◽  
Author(s):  
M. D. Gladstone
Keyword(s):  
Recursion Scheme ◽  
Projection Functions ◽  
Primitive Recursive

This paper resolves 3 problems left open by R. M. Robinson in [3].We recall that the set of primitive recursive functions is the closure under (i) substitution (or “composition”), and (ii) recursion, of the set P consisting of the zero, successor and projection functions (see any textbook, for instance p. 120 of [2]).

scholarly journals Primitive recursive computations.

1967 ◽  
Vol 8 (4) ◽  
pp. 311-317 ◽  
Author(s):  
Stephen H. McCleary
Keyword(s):  
Primitive Recursive
Sign in / Sign up

Export Citation Format

Share Document