Displaying similar documents to “Mizar Analysis of Algorithms: Preliminaries”

Free Term Algebras

Grzegorz Bancerek (2012)

Formalized Mathematics

Similarity:

We interoduce a new characterization of algebras of normal forms of term rewriting systems [35] as algerbras of term free in itself (any function from free generators into the algebra generates endomorphism of the algebra). Introduced algebras are free in classes of algebras satisfying some sets of equalities. Their universes are subsets of all terms and the denotations of operation symbols are partially identical with the operations of construction of terms. These algebras are compiler...

A semantic construction of two-ary integers

Gabriele Ricci (2005)

Discussiones Mathematicae - General Algebra and Applications

Similarity:

To binary trees, two-ary integers are what usual integers are to natural numbers, seen as unary trees. We can represent two-ary integers as binary trees too, yet with leaves labelled by binary words and with a structural restriction. In a sense, they are simpler than the binary trees, they relativize. Hence, contrary to the extensions known from Arithmetic and Algebra, this integer extension does not make the starting objects more complex. We use a semantic construction to get this extension....

An algorithm for free algebras

Jaroslav Ježek (2010)

Commentationes Mathematicae Universitatis Carolinae

Similarity:

We present an algorithm for constructing the free algebra over a given finite partial algebra in the variety determined by a finite list of equations. The algorithm succeeds whenever the desired free algebra is finite.