<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

Pubblicato online: 30 giu 2014

Pagine: 125 - 155

Ricevuto: 13 giu 2014

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

Parole chiave
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

Pubblicato online: 30 giu 2014

Pagine: 125 - 155

Ricevuto: 13 giu 2014

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

Parole chiaveconstruction 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)

Parole chiave
construction degree, context, translation, endomorphism