scholarly journals Normal-order reduction grammars

2017 ◽  
Vol 27 ◽  
Author(s):  
MACIEJ BENDKOWSKI
Keyword(s):  
Upper Bound ◽  
Generating Functions ◽  
Order Reduction ◽  
Combinatory Logic ◽  
Recursive Method ◽  
Normal Order ◽  
Regular Tree ◽  
Tree Grammar ◽  
Primitive Recursive

AbstractWe present an algorithm which, for given n, generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set {S, K} of primitive combinators, requiring exactly n normal-order reduction steps to normalize. As a consequence of Curry and Feys's standardization theorem, our reduction grammars form a complete syntactic characterization of normalizing combinatory logic terms. Using them, we provide a recursive method of constructing ordinary generating functions counting the number of SK-combinators reducing in n normal-order reduction steps. Finally, we investigate the size of generated grammars giving a primitive recursive upper bound.

scholarly journals A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations

2008 ◽  
Vol 18 (3) ◽  
pp. 501-553 ◽  
Author(s):  
DAVID SABEL ◽  
MANFRED SCHMIDT-SCHAUSS
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Order Reduction ◽  
Single Step ◽  
Program Transformations ◽  
Normal Order ◽  
Choice Context ◽  
Contextual Equivalence ◽  
Fairness Condition

We present a higher-order call-by-need lambda calculus enriched with constructors, case expressions, recursive letrec expressions, a seq operator for sequential evaluation and a non-deterministic operator amb that is locally bottom-avoiding. We use a small-step operational semantics in the form of a single-step rewriting system that defines a (non-deterministic) normal-order reduction. This strategy can be made fair by adding resources for book-keeping. As equational theory, we use contextual equivalence (that is, terms are equal if, when plugged into any program context, their termination behaviour is the same), in which we use a combination of may- and must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations with respect to normal-order reduction are the same as for fair normal-order reduction. We develop a number of proof tools for proving correctness of program transformations. In particular, we prove a context lemma for both may- and must- convergence that restricts the number of contexts that need to be examined for proving contextual equivalence. Combining this with so-called complete sets of commuting and forking diagrams, we show that all the deterministic reduction rules and some additional transformations preserve contextual equivalence. We also prove a standardisation theorem for fair normal-order reduction. The structure of the ordering ≤c is also analysed, and we show that Ω is not a least element and ≤c already implies contextual equivalence with respect to may-convergence.

Solving Regular Tree Grammar Based Constraints

2001 ◽  
pp. 213-233 ◽  
Author(s):  
Yanhong A. Liu ◽  
Ning Li ◽  
Scott D. Stoller
Keyword(s):  
Regular Tree ◽  
Tree Grammar

scholarly journals PRESBURGER ARITHMETIC, RATIONAL GENERATING FUNCTIONS, AND QUASI-POLYNOMIALS

2015 ◽  
Vol 80 (2) ◽  
pp. 433-449 ◽  
Author(s):  
KEVIN WOODS
Keyword(s):  
Generating Functions ◽  
Counting Function ◽  
Order Theory ◽  
Characteristic Functions ◽  
Presburger Arithmetic ◽  
First Order ◽  
First Order Theory ◽  
Rational Generating Function ◽  
Rational Generating Functions

AbstractPresburger arithmetic is the first-order theory of the natural numbers with addition (but no multiplication). We characterize sets that can be defined by a Presburger formula as exactly the sets whose characteristic functions can be represented by rational generating functions; a geometric characterization of such sets is also given. In addition, ifp= (p1, . . . ,pn) are a subset of the free variables in a Presburger formula, we can define a counting functiong(p) to be the number of solutions to the formula, for a givenp. We show that every counting function obtained in this way may be represented as, equivalently, either a piecewise quasi-polynomial or a rational generating function. Finally, we translate known computational complexity results into this setting and discuss open directions.

scholarly journals Ramsey-like cardinals II

2011 ◽  
Vol 76 (2) ◽  
pp. 541-560 ◽  
Author(s):  
Victoria Gitman ◽  
P. D. Welch
Keyword(s):  
Upper Bound ◽  
Large Cardinals ◽  
Large Cardinal ◽  
Core Model ◽  
Consistency Strength ◽  
The Core ◽  
Countable Ordinal ◽  
Elementary Embeddings ◽  
Remarkable Cardinals

AbstractThis paper continues the study of the Ramsey-like large cardinals introduced in [5] and [14]. Ramsey-like cardinals are defined by generalizing the characterization of Ramsey cardinals via the existence of elementary embeddings. Ultrafilters derived from such embeddings are fully iterable and so it is natural to ask about large cardinal notions asserting the existence of ultrafilters allowing only α-many iterations for some countable ordinal α. Here we study such α-iterable cardinals. We show that the α-iterable cardinals form a strict hierarchy for α ≤ ω1, that they are downward absolute to L for , and that the consistency strength of Schindler's remarkable cardinals is strictly between 1-iterable and 2-iterable cardinals.We show that the strongly Ramsey and super Ramsey cardinals from [5] are downward absolute to the core model K. Finally, we use a forcing argument from a strongly Ramsey cardinal to separate the notions of Ramsey and virtually Ramsey cardinals. These were introduced in [14] as an upper bound on the consistency strength of the Intermediate Chang's Conjecture.

Place probabilities in normal order statistics models for horse races

1981 ◽  
Vol 18 (04) ◽  
pp. 839-852 ◽  
Author(s):  
R. J. Henery
Keyword(s):  
Order Statistics ◽  
Series Expansion ◽  
Taylor Series ◽  
Upper Bound ◽  
Taylor Series Expansion ◽  
Distribution Functions ◽  
Normal Order ◽  
Increasing Failure Rate ◽  
Normal Populations ◽  
Independent Observations

Independent observations X 0, X 1…, X N+1 are drawn from each of N populations whose distribution functions F(x – θi ) have means θ i , 0 ≦ i < N, and we wish to calculate the probability P k;N that X 0 is the k th largest observation. For normal populations an approximation is given for P K;N based on a Taylor series expansion in the θ 's. If F(x) has an increasing failure rate, as is the case for the normal, an upper bound can be given for the ‘win' probability P 1;N Some moment relations for normal order statistics are also given.

Closed Fragments of Provability Logics of Constructive Theories

2008 ◽  
Vol 73 (3) ◽  
pp. 1081-1096 ◽  
Author(s):  
Albert Visser
Keyword(s):  
Provability Logic ◽  
Primitive Recursive

AbstractIn this paper we give a new proof of the characterization of the closed fragment of the provability logic of Heyting's Arithmetic. We also provide a characterization of the closed fragment of the provability logic of Heyting's Arithmetic plus Markov's Principle and Heyting's Arithmetic plus Primitive Recursive Markov's Principle.

A proof-theoretic characterization of the primitive recursive set functions

1992 ◽  
Vol 57 (3) ◽  
pp. 954-969 ◽  
Author(s):  
Michael Rathjen
Keyword(s):  
Set Theory ◽  
Elementary Proof ◽  
Weak Version ◽  
Definable Set ◽  
Set Functions ◽  
Theoretic Characterization ◽  
Universe Of Sets ◽  
Set Function ◽  
Primitive Recursive

AbstractLet KP− be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V ≔ universe of sets) be a Δ0-definable set function, i.e. there is a Δ0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and V ⊨ ∀x∃!yφ(x, y). In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection of those functions which are Σ1-definable in KP− + Σ1-Foundation + ∀x∃!yφ(x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of Δ0-Dependent Choices to the latter theory.

Sign in / Sign up

Export Citation Format

Share Document