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 degree of construction as a number of used operation symbols is defined. Next, the term context is investigated. An x-context is a term whic...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2014-06-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.2478/forma-2014-0015 |
| id |
doaj-8af1807ebdc54d2b8fdb4cfd360f182e |
|---|---|
| record_format |
Article |
| spelling |
doaj-8af1807ebdc54d2b8fdb4cfd360f182e2021-09-05T21:01:03ZengSciendoFormalized Mathematics1898-99342014-06-0122212515510.2478/forma-2014-0015forma-2014-0015Term ContextBancerek Grzegorz0Association of Mizar Users Białystok, PolandTwo 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.https://doi.org/10.2478/forma-2014-0015construction degreecontexttranslationendomorphism08a3503b35 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Bancerek Grzegorz |
| spellingShingle |
Bancerek Grzegorz Term Context Formalized Mathematics construction degree context translation endomorphism 08a35 03b35 |
| author_facet |
Bancerek Grzegorz |
| author_sort |
Bancerek Grzegorz |
| title |
Term Context |
| title_short |
Term Context |
| title_full |
Term Context |
| title_fullStr |
Term Context |
| title_full_unstemmed |
Term Context |
| title_sort |
term context |
| publisher |
Sciendo |
| series |
Formalized Mathematics |
| issn |
1898-9934 |
| publishDate |
2014-06-01 |
| description |
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. |
| topic |
construction degree context translation endomorphism 08a35 03b35 |
| url |
https://doi.org/10.2478/forma-2014-0015 |
| work_keys_str_mv |
AT bancerekgrzegorz termcontext |
| _version_ |
1717781728453459968 |