Терм: различия между версиями

Материал из WEGA
Перейти к навигации Перейти к поиску
Нет описания правки
Нет описания правки
 
Строка 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>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>.
Термы ''[[конвергентные термы|конвергентны]]'', если их нормальные формы совпадают.
Термы ''[[конвергентные термы|конвергентны]]'', если их нормальные формы совпадают.


Строка 33: Строка 33:
''[[дерево выражения]]'' и ''[[дэг выражения]]''.
''[[дерево выражения]]'' и ''[[дэг выражения]]''.
==Литература==
==Литература==
[Евстигнеев-Касьянов/94]
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.

Текущая версия от 10:45, 20 сентября 2011

Терм (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]. Термы конвергентны, если их нормальные формы совпадают.

В качестве графововых представлений терма используются дерево выражения и дэг выражения.

Литература

  • Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.