<abstract xmlns="http://www.w3.org/1999/xhtml"><p>Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The degree of construction as a number of used operation symbols is defined. Next, the term context is investigated. An <italic>x-context</italic> is a term which includes a variable <italic>x</italic> once only. The compound term is <italic>x-context</italic> iff the argument terms include an <italic>x-context</italic> once only. The context induction is shown and used many times. As a key concept, the context substitution is introduced. Finally, the translations and endomorphisms are expressed by context substitution.</p></abstract>

Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The degree of construction as a number of used operation symbols is defined. Next, the term context is investigated. An x-context is a term which includes a variable x once only. The compound term is x-context iff the argument terms include an x-context once only. The context induction is shown and used many times. As a key concept, the context substitution is introduced. Finally, the translations and endomorphisms are expressed by context substitution.

Term Context

Association of Mizar Users Białystok, Poland

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"Term Context"}

Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The...

Term Context

Publicado en línea: 30 jun 2014

Páginas: 125 - 155

Recibido: 13 jun 2014

DOI: https://doi.org/10.2478/forma-2014-0015

Palabras clave
construction degree, context, translation, endomorphism

© 2014 Grzegorz Bancerek

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Term Context

Publicado en línea: 30 jun 2014

Páginas: 125 - 155

Recibido: 13 jun 2014

DOI: https://doi.org/10.2478/forma-2014-0015

Palabras claveconstruction degree, context, translation, endomorphism

© 2014 Grzegorz Bancerek

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Palabras clave
construction degree, context, translation, endomorphism