scholarly journals Primitive recursion in the abstract

2020 ◽  
Vol 30 (1) ◽  
pp. 33-43
Author(s):  
Daniel Leivant ◽  
Jean-Yves Marion
Keyword(s):  
Computational Complexity ◽  
Free Algebra ◽  
Generic Programming ◽  
Underlying Structure ◽  
Free Algebras ◽  
Primitive Recursion ◽  
Function Definition ◽  
Primitive Recursive

AbstractRecurrence can be used as a function definition schema for any nontrivial free algebra, yielding the same computational complexity in all cases. We show that primitive-recursive computing is in fact independent of free algebras altogether, and can be characterized by a generic programming principle, namely the control of iteration by the depletion of finite components of the underlying structure.

Finitely generated free Heyting algebras

1986 ◽  
Vol 51 (1) ◽  
pp. 152-165 ◽  
Author(s):  
Fabio Bellissima
Keyword(s):  
Free Algebra ◽  
Kripke Semantics ◽  
Heyting Algebras ◽  
Free Algebras ◽  
Finitely Generated ◽  
Algebraic Properties

AbstractThe aim of this paper is to give, using the Kripke semantics for intuitionism, a representation of finitely generated free Heyting algebras. By means of the representation we determine in a constructive way some set of “special elements” of such algebras. Furthermore, we show that many algebraic properties which are satisfied by the free algebra on one generator are not satisfied by free algebras on more than one generator.

Finite Projective Distributive Lattices

1970 ◽  
Vol 13 (1) ◽  
pp. 139-140 ◽  
Author(s):  
G. Grätzer ◽  
B. Wolk
Keyword(s):  
Distributive Lattice ◽  
Free Algebra ◽  
Distributive Lattices ◽  
Free Algebras ◽  
Algebra Ii

The theorem stated below is due to R. Balbes. The present proof is direct; it uses only the following two well-known facts: (i) Let K be a category of algebras, and let free algebras exist in K; then an algebra is projective if and only if it is a retract of a free algebra, (ii) Let F be a free distributive lattice with basis {xi | i ∊ I}; then ∧(xi | i ∊ J0) ≤ ∨(xi | i ∊ J1) implies J0∩J1≠ϕ. Note that (ii) implies (iii): If for J0 ⊆ I, a, b ∊ F, ∧(xi | i ∊ J0)≤a ∨ b, then ∧ (xi | i ∊ J0)≤ a or b.

scholarly journals Primitive recursive algebraic theories and program schemes

1977 ◽  
Vol 17 (2) ◽  
pp. 207-233 ◽  
Author(s):  
W. Kühnel ◽  
J. Meseguer ◽  
M. Pfender ◽  
I. Sols
Keyword(s):  
Programming Language ◽  
Generation Process ◽  
Recursive Functions ◽  
Algebraic Theories ◽  
Primitive Recursion ◽  
Recursive Theory ◽  
Carry Over ◽  
Primitive Recursive

We introduce primitive recursion as a generation process for arrows of algebraic theories in the sense of Lawvere and carry over important results on algebraic theories and functorial semantics to the enriched setting of “primitive recursive algebra”: existence of free primitive recursive theories and of theories presented by operations and equations on primitive recursive functions; existence of free models presented by generators and equations. Finally semantical correctness of translations is reduced to correctness for the basic operations. There is a connection to the theory of program schemes: program schemes involving primitive recursion correspond to arrows of a primitive recursive theory freely generated over a graph of basic operations. This theory T can be viewed as a programming language with “arithmetics” given by the basic operations and with DO-loops. A machine loaded with a compiler for T can be interpreted as a T-model in Lawvere's sense, preserving primitive recursion.

scholarly journals Computation of minimal homogeneous generating sets and minimal standard bases for ideals of free algebras

2018 ◽  
Vol 25 (3) ◽  
pp. 451-459
Author(s):  
Huishi Li
Keyword(s):  
Free Algebra ◽  
Standard Basis ◽  
Free Algebras ◽  
Grobner Basis ◽  
Finitely Generated ◽  
Generating Set ◽  
Standard Bases ◽  
Generating Sets ◽  
Monomial Ordering ◽  
Minimal Standard

AbstractLet {K\langle X\rangle=K\langle X_{1},\ldots,X_{n}\rangle} be the free algebra generated by {X=\{X_{1},\ldots,X_{n}\}} over a field K. It is shown that, with respect to any weighted {\mathbb{N}}-gradation attached to {K\langle X\rangle}, minimal homogeneous generating sets for finitely generated graded two-sided ideals of {K\langle X\rangle} can be algorithmically computed, and that if an ungraded two-sided ideal I of {K\langle X\rangle} has a finite Gröbner basis {{\mathcal{G}}} with respect to a graded monomial ordering on {K\langle X\rangle}, then a minimal standard basis for I can be computed via computing a minimal homogeneous generating set of the associated graded ideal {\langle\mathbf{LH}(I)\rangle}.

scholarly journals Ideal Dasar Prima Dalam Aljabar Atas Suatu Ring Komutatif

2018 ◽  
Vol 7 (2) ◽  
pp. 79-86
Author(s):  
Khurul Wardati
Keyword(s):  
Commutative Ring ◽  
Free Algebra ◽  
Free Algebras

Definisi ideal dasar dan ideal bebas dalam aljabar bebas atas ring komutatif dengan elemen satuan adalah ekuivalen. Namun, ideal dasar dalam suatu aljabar tak bebas belum tentu merupakan ideal bebas, sementara ideal bebas pasti ideal dasar. Artikel ini membahas beberapa sifat ideal dasar prima dalam aljabar tak bebas atas ring komutatif dengan elemen satuan. [The definitions of basic ideal and free ideal in free algebras over a unital commutative ring are equivalen. However, a basic ideal in the non-free algebra is not neceearily a free ideal, while any free ideal is definitely a basic ideal. This paper will discuss some properties of prime basic ideal in non-free algebras over a unital commutative ring.]

Functionals defined by transfinite recursion

1965 ◽  
Vol 30 (2) ◽  
pp. 155-174 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Functional Equations ◽  
Partial Ordering ◽  
Closure Properties ◽  
Primitive Recursive Arithmetic ◽  
Primitive Recursion ◽  
Definition Of ◽  
Second Order Systems ◽  
Transfinite Recursion ◽  
Primitive Recursive ◽  
Elementary Closure

This paper deals mainly with quantifier-free second order systems (i.e., with free variables for numbers and functions, and constants for numbers, functions, and functionals) whose basic rules are those of primitive recursive arithmetic together with definition of functionals by primitive recursion and explicit definition. Precise descriptions are given in §2. The additional rules have the form of definition by transfinite recursion up to some ordinal ξ (where ξ is represented by a primitive recursive (p.r.) ordering). In §3 we discuss some elementary closure properties (under rules of inference and definition) of systems with recursion up to ξ. Let Rξ denote (temporarily) the system with recursion up to ξ. The main results of this paper are of two sorts:Sections 5–7 are concerned with less elementary closure properties of the systems Rξ. Namely, we show that certain classes of functional equations in Rη can be solved in Rη for some explicitly determined η < ε(η) (the least ε-number > ξ). The classes of functional equations considered all have roughly the form of definition by recursion on the partial ordering of unsecured sequences of a given functional F, or on some ordering which is obtained from this by simple ordinal operations. The key lemma (Theorem 1) needed for the reduction of these equations to transfinite recursion is simply a sharpening of the Brouwer-Kleene idea.

scholarly journals Editorial

2001 ◽  
Vol 11 (1) ◽  
pp. 1-1
Author(s):  
Daniel Leivant ◽  
Bob Constable
Keyword(s):  
Computational Complexity ◽  
Functional Programming ◽  
Linear Logic ◽  
Theoretical Computer Science ◽  
Theory And Practice ◽  
Complexity Classes ◽  
Higher Order Logic ◽  
Database Theory ◽  
Implicit Computational Complexity ◽  
Primitive Recursive

This issue of the Journal of Functional Programming is dedicated to work presented at the Workshop on Implicit Computational Complexity in Programming Languages, affiliated with the 1998 meeting of the International Conference on Functional Programming in Baltimore.Several machine-independent approaches to computational complexity have been developed in recent years; they establish a correspondence linking computational complexity to conceptual and structural measures of complexity of declarative programs and of formulas, proofs and models of formal theories. Examples include descriptive complexity of finite models, restrictions on induction in arithmetic and related first order theories, complexity of set-existence principles in higher order logic, and specifications in linear logic. We refer to these approaches collectively as Implicit Computational Complexity. This line of research provides a framework for a streamlined incorporation of computational complexity into areas such as formal methods in software development, programming language theory, and database theory.A fruitful thread in implicit computational complexity is based on exploring the computational complexity consequences of introducing various syntactic control mechanisms in functional programming, including restrictions (akin to static typing) on scoping, data re-use (via linear modalities), and iteration (via ramification of data). These forms of control, separately and in combination, can certify bounds on the time and space resources used by programs. In fact, all results in this area establish that each restriction considered yields precisely a major computational complexity class. The complexity classes thus obtained range from very restricted ones, such as NC and Alternating logarithmic time, through the central classes Poly-Time and Poly-Space, to broad classes such as the Elementary and the Primitive Recursive functions.Considerable effort has been invested in recent years to relax as much as possible the structural restrictions considered, allowing for more exible programming and proof styles, while still guaranteeing the same resource bounds. Notably, more exible control forms have been developed for certifying that functional programs execute in Poly-Time.The 1998 workshop covered both the theoretical foundations of the field and steps toward using its results in various implemented systems, for example in controlling the computational complexity of programs extracted from constructive proofs. The five papers included in this issue nicely represent this dual concern of theory and practice. As they are going to print, we should note that the field of Implicit Computational Complexity continues to thrive: successful workshops dedicated to it were affiliated with both the LICS'99 and LICS'00 conferences. Special issues, of Information and Computation dedicated to the former, and of Theoretical Computer Science to the latter, are in preparation.

scholarly journals The persistence of universal formulae in free algebras

1987 ◽  
Vol 36 (1) ◽  
pp. 11-17 ◽  
Author(s):  
Anthony M. Gaglione ◽  
Dennis Spellman
Keyword(s):  
Wreath Product ◽  
Free Algebra ◽  
Variety Of Algebras ◽  
Free Algebras ◽  
Product Construction

Gilbert Baumslag, B.H. Neumann, Hanna Neumann, and Peter M. Neumann successfully exploited their concept of discrimination to obtain generating groups of product varieties via the wreath product construction. We have discovered this same underlying concept in a somewhat different context. Specifically, let V be a non-trivial variety of algebras. For each cardinal α let Fα(V) be a V-free algebra of rank α. Then for a fixed cardinal r one has the equivalence of the following two statements:(1) Fr(V) discriminates V. (1*) The Fs(V) satisfy the same universal sentences for all s≥r. Moreover, we have introduced the concept of strong discrimination in such a way that for a fixed finite cardinal r the following two statements are equivalent:(2) Fr(V) strongly discriminates V. (2*) The Fs(V) satisfy the same universal formulas for all s ≥ r whenever elements of Fr(V) are substituted for the unquantified variables. On the surface (2) and (2*) appear to be stronger conditions than (1) and (1*). However, we have shown that for particular varieties (of groups) (2) and (2*) are no stronger than (1) and (1*).

Primitive Recursion with Existential Types1

1993 ◽  
Vol 19 (1-2) ◽  
pp. 201-222
Author(s):  
Pawel Urzyczyn
Keyword(s):  
Standard Approach ◽  
Halting Problem ◽  
Primitive Recursion ◽  
Representation Of Integers ◽  
Existential Quantification ◽  
Primitive Recursive ◽  
Recursive Definitions ◽  
Recursive Set

We consider computability over abstract structures with help of primitive recursive definitions (an appropriate modification of Gödel’s system T). Unlike the standard approach, we do not assume any fixed representation of integers, but instead we allow primitive recursion to be polymorphic, so that iteration is performed with help of counters viewed as objects of an abstract type Int of arbitrary (hidden) implementation. This approach involves the use of existential quantification in types, following the ideas of Mitchell and Plotkin. We show that the halting problem over finite interpretations is primitive recursive for each program involving primitive recursive definitions. Conversely, each primitive recursive set of interpretations is defined by the termination property of some program.

The substitution method

1965 ◽  
Vol 30 (2) ◽  
pp. 175-192 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Free Variable ◽  
Order System ◽  
Conservative Extension ◽  
Substitution Method ◽  
Recursive Definition ◽  
First Order ◽  
Variable Elimination ◽  
Primitive Recursion ◽  
Definition Of ◽  
Primitive Recursive

This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system S framed in the ε-calculus [2] the problem is to associate a system S' without bound variables and an effective procedure for transforming derivations in S into derivations in S′. The transform of a formula A derived in S is to be an “ε-substitution instance” of A, i.e. it is obtained by replacing terms εxB(x) in A by terms of S′. In general the choice of these terms will depend on the particular derivation of A, and not on A alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of A should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in S′; on the other hand, it generalizes Hilbert's formulation since S′ need not be restricted to finitist systems.The bound variable elimination procedure can always be taken to be primitive recursive in (the Gödel number of) the derivation of A. Constructions which transcend primitive recursion can simply be built into S′.In this paper we show that if S′ is taken to be a second order system with constants for functionals, then the existence of suitable ε-substitution instances can be expressed by the solvability of certain functional equations in S′. We deal with two cases here. If S is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for S′ the free variable part S* of S with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of S*.

Sign in / Sign up

Export Citation Format

Share Document