Open Access

Term Context

Formalized Mathematics's Cover Image
Formalized Mathematics
Special Issue: 25 years of the Mizar Mathematical Library

Cite

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.

eISSN:
1898-9934
Language:
English
Publication timeframe:
4 times per year
Journal Subjects:
Computer Sciences, other, Mathematics, General Mathematics