Терм: различия между версиями
Glk (обсуждение | вклад) (Создана новая страница размером '''Терм''' (''Term'') - правильно построенная формула над некоторым алфавитом <math>\...) |
KEV (обсуждение | вклад) Нет описания правки |
||
| Строка 1: | Строка 1: | ||
'''Терм''' (''Term'') - | '''Терм''' (''[[Term]]'') - | ||
правильно построенная формула над некоторым алфавитом <math>\Sigma</math>, | правильно построенная формула над некоторым [[алфавит|алфавитом]] <math>\Sigma</math>, | ||
образованным из множества символов переменных <math>V</math> и символов | образованным из множества символов переменных <math>V</math> и символов | ||
<math>r</math>-арных функций <math>\Sigma_r</math>, где <math>r\geq 0</math> | <math>r</math>-арных функций <math>\Sigma_r</math>, где <math>r\geq 0</math> - арность функций | ||
(количество ее "аргументов"). | (количество ее "аргументов"). | ||
Если терм <math>t</math> имеет вид | Если терм <math>t</math> имеет вид | ||
<math>f(t_1, t_2, \ldots, t_r),</math> | <math>f(t_1, t_2, \ldots, t_r), </math> | ||
где <math>f \in \Sigma_r</math>, <math>r>0</math>, | где <math>f \in \Sigma_r</math>, <math>r>0</math>, | ||
то <math>f</math> называется ''внешним'' (''корневым'') | то <math>f</math> называется ''[[внешний терм|внешним]]'' (''[[корневой терм|корневым]]'') | ||
символом терма <math>t</math>, а термы <math>t_1</math>, <math>t_2</math>, <math>\ldots</math>, <math>t_r</math> | символом терма <math>t</math>, а термы <math>t_1</math>, <math>t_2</math>, <math>\ldots</math>, <math>t_r</math> | ||
и их подтермы | и их подтермы | ||
- ''[[подтерм|подтермами]]'' терма <math>t</math>. Терм <math>t</math> | |||
- ''[[замкнутый терм|замкнутый]]'', если в нем нет переменных, и ''[[линейный терм|линейный]]'', | |||
если он не содержит двух вхождений одной и той же переменной. | если он не содержит двух вхождений одной и той же переменной. | ||
Терм <math>t</math> называется ''редуцируемым'' (относительно некоторой | Терм <math>t</math> называется ''[[редуцируемый терм|редуцируемым]]'' (относительно некоторой | ||
''системы переписывания термов'' <math>R</math>), | ''[[система переписывания термов|системы переписывания термов]]'' <math>R</math>), | ||
если существует такой терм <math>s</math>, | если существует такой терм <math>s</math>, | ||
отличный от <math>t</math>, что <math>t \longrightarrow_R s</math>, и | отличный от <math>t</math>, что <math>t \longrightarrow_R s</math>, и | ||
''нередуцируемым'' (или ''тупиковым'') в противном случае. | ''нередуцируемым'' (или ''[[тупиковый терм|тупиковым]]'') в противном случае. | ||
Термы <math>t</math> и <math>s</math> | Термы <math>t</math> и <math>s</math> | ||
''эквивалентны'', если | ''[[эквивалентные термы|эквивалентны]]'', если | ||
<math>t \longrightarrow_R s</math> или <math>s \longrightarrow_R t</math>. | <math>t \longrightarrow_R s</math> или <math>s \longrightarrow_R t</math>. | ||
Если <math>t \longrightarrow_R s</math> и <math>s</math> нередуцируемый, то | Если <math>t \longrightarrow_R s</math> и <math>s</math> нередуцируемый, то | ||
<math>s</math> называется ''нормальной формой'' терма <math>t</math>. | <math>s</math> называется ''[[нормальная форма терма|нормальной формой]]'' терма <math>t</math>. | ||
Термы ''конвергентны'', если их нормальные формы совпадают. | Термы ''[[конвергентные термы|конвергентны]]'', если их нормальные формы совпадают. | ||
В качестве графововых представлений терма используются | В качестве графововых представлений терма используются | ||
''дерево выражения'' и ''дэг выражения''. | ''[[дерево выражения]]'' и ''[[дэг выражения]]''. | ||
==Литература== | ==Литература== | ||
[Евстигнеев-Касьянов/94] | [Евстигнеев-Касьянов/94] | ||
Версия от 12:28, 7 февраля 2010
Терм (Term) - правильно построенная формула над некоторым алфавитом [math]\displaystyle{ \Sigma }[/math], образованным из множества символов переменных [math]\displaystyle{ V }[/math] и символов [math]\displaystyle{ r }[/math]-арных функций [math]\displaystyle{ \Sigma_r }[/math], где [math]\displaystyle{ r\geq 0 }[/math] - арность функций (количество ее "аргументов").
Если терм [math]\displaystyle{ t }[/math] имеет вид
[math]\displaystyle{ f(t_1, t_2, \ldots, t_r), }[/math]
где [math]\displaystyle{ f \in \Sigma_r }[/math], [math]\displaystyle{ r\gt 0 }[/math], то [math]\displaystyle{ f }[/math] называется внешним (корневым) символом терма [math]\displaystyle{ t }[/math], а термы [math]\displaystyle{ t_1 }[/math], [math]\displaystyle{ t_2 }[/math], [math]\displaystyle{ \ldots }[/math], [math]\displaystyle{ t_r }[/math] и их подтермы - подтермами терма [math]\displaystyle{ t }[/math]. Терм [math]\displaystyle{ t }[/math] - замкнутый, если в нем нет переменных, и линейный, если он не содержит двух вхождений одной и той же переменной.
Терм [math]\displaystyle{ t }[/math] называется редуцируемым (относительно некоторой системы переписывания термов [math]\displaystyle{ R }[/math]), если существует такой терм [math]\displaystyle{ s }[/math], отличный от [math]\displaystyle{ t }[/math], что [math]\displaystyle{ t \longrightarrow_R s }[/math], и нередуцируемым (или тупиковым) в противном случае. Термы [math]\displaystyle{ t }[/math] и [math]\displaystyle{ s }[/math] эквивалентны, если [math]\displaystyle{ t \longrightarrow_R s }[/math] или [math]\displaystyle{ s \longrightarrow_R t }[/math].
Если [math]\displaystyle{ t \longrightarrow_R s }[/math] и [math]\displaystyle{ s }[/math] нередуцируемый, то [math]\displaystyle{ s }[/math] называется нормальной формой терма [math]\displaystyle{ t }[/math]. Термы конвергентны, если их нормальные формы совпадают.
В качестве графововых представлений терма используются дерево выражения и дэг выражения.
Литература
[Евстигнеев-Касьянов/94]