Терм — как выражение формального языка (системы)

Привет, Вы узнаете о том , что такое терм, Разберем основные их виды и особенности использования. Еще будет много подробных примеров и описаний. Для того чтобы лучше понимать что такое терм , настоятельно рекомендую прочитать все из категории Логика.

терм — выражение формального языка (системы) специального вида. По аналогии с естественным языком, где именная группа ссылается на объект, а целое предложение ссылается на факт, в математической логике терм обозначает математический объект, а формула обозначает математический факт. В частности, термы появляются как компоненты формулы.

Терм первого порядка рекурсивно определяется из символов постоянных, переменных и функций . Выражение, полученное путем применения предикатного символа к соответствующему количеству термов, называется логическим атомом, значение которого в двузначной логике на основе логической интерпретации оценивается как «истина» или «ложь ». Например, — это терм, построенный из константы 1, переменной x и символов двоичной функции + и ∗ ; это часть атомарной формулы , которая принимает значение «истина» для любого вещественного x.

Помимо логики, термы играют важную роль в универсальной алгебре и системах переписывания.

Множество термов сигнатуры , где R — множество предикатов, F — множество функций, а μ — отображение арности для Σ , определяется индуктивно:

1. переменные являются термами сигнатуры Σ
2. если терм сигнатуры Σ , f∈F и μ(f)=n, то — терм сигнатуры Σ .

Запись при n=0 обозначает Θ. В частности, из пункта 2 получаем, что символ константы сигнатуры Σ является термом сигнатуры Σ.

Слева направо: древовидная структура термина ( n ⋅( n +1))/2 и n ⋅(( n +1)/2)

При наличии множества V переменных символов, множества C постоянных символов и множеств F _n символов n - арных функций, также называемых символами операторов, для каждого натурального числа n ≥ 1 множество (несортированных членов первого порядка) T рекурсивно определяется как наименьшее множество со следующими свойствами: ^{[ 1 ]}

• каждый переменный символ является термином: V ⊆ T ,
• каждый постоянный символ является термином: C ⊆ T ,
• из каждых n членов t ₁ ,..., t _n и каждого n -арного функционального символа f ∈ F _n можно построить больший член f ( t ₁ , ..., t _{n ).}

Используя интуитивную псевдограмматическую запись, это иногда записывается так:

t ::= x | c | f ( t ₁ , ..., t _n ).

Сигнатура термина «язык» описывает, какие наборы функциональных символов F n _{используются} . Хорошо известными примерами являются унарные функциональные символы sin , cos ∈ F ₁ и бинарные функциональные символы +, −, ⋅, / ∈ F ₂ . Тернарные операции и функции более высокой арности возможны, но на практике встречаются редко. Многие авторы рассматривают константные символы как 0-арные функциональные символы F ₀ , поэтому для них не требуется специального синтаксического класса.

Термин обозначает математический объект из области дискурса . Константа c обозначает именованный объект из этой области, переменная x пробегает объекты в этой области, а n -арная функция f отображает n - кортежи объектов в объекты. Например, если n ∈ V является символом переменной, 1 ∈ C является символом константы, а add ∈ F ₂ является символом бинарной функции, то n ∈ T , 1 ∈ T , и (следовательно) add ( n , 1) ∈ T по правилу построения первого, второго и третьего терминов соответственно. Последний термин обычно записывается как n + 1 , используя инфиксную нотацию и более распространенный символ оператора + для удобства.

Первоначально логики определяли термин как строку символов, подчиняющуюся определенным правилам построения. ^{[ 2 ]} Однако, поскольку концепция дерева стала популярной в информатике, оказалось удобнее представлять термин как дерево. Например, несколько различных строк символов, таких как «, обозначают один и тот же термин и соответствуют одному и тому же дереву, а именно левому дереву на рисунке выше. Отделяя древовидную структуру термина от его графического представления на бумаге, легко учесть скобки (являющиеся лишь представлением, а не структурой) и невидимые операторы умножения (существующие только в структуре, а не в представлении).

Два термина считаются структурно , буквально или синтаксически равными, если они соответствуют одному и тому же дереву. Например, левое и правое деревья на рисунке выше являются структурно неравными терминами, хотя их можно считать « семантически равными », поскольку они всегда дают одно и то же значение в рациональной арифметике . В то время как структурное равенство можно проверить без знания значения символов, семантическое равенство невозможно. Если функция / интерпретируется, например, не как рациональное, а как усечение целочисленного деления, то при n = 2 левый и правый термины будут иметь значение 3 и 2 соответственно. Структурно равные термины должны согласовываться в именах переменных.

Напротив, термин t называется переименованием или вариантом термина u , если последний получился в результате последовательного переименования всех переменных первого, т. е. если u = tσ для некоторой переименования-замены σ. В этом случае u также является переименованием t , поскольку переименование-замена σ имеет обратный σ ⁻¹ , и t = uσ ⁻¹ . Тогда оба термина также называются равными по модулю переименования . Во многих контекстах конкретные имена переменных в термине не имеют значения, например, аксиома коммутативности для сложения может быть сформулирована как x + y = y + x или как a + b = b + a ; в таких случаях вся формула может быть переименована, в то время как произвольный подтерм обычно не может, например, x + y = b + a не является допустимой версией аксиомы коммутативности.

Множество переменных терма t обозначается как vars ( t ). Терм, не содержащий переменных, называется основным термом ; терм, не содержащий нескольких вхождений одной переменной, называется линейным термом . Например, 2+2 является основным термом и, следовательно, также линейным термом, x ⋅( n +1) — линейный терм, n ⋅( n +1) — нелинейный терм. Эти свойства важны, например, при переписывании терма .

При заданной сигнатуре для символов функций множество всех членов образует алгебру свободных членов . Множество всех основных членов образует исходную алгебру членов .

Сокращая число констант как f ₀ , а число символов i- арной функции как f _i , число θ _h различных основных членов высоты до h можно вычислить с помощью следующей рекурсивной формулы:

• θ ₀ = f ₀ , поскольку основной член высоты 0 может быть только константой,
• , поскольку основной член высотой до h + 1 может быть получен путем сложения любых i основных членов высотой до h с использованием символа i- арной корневой функции. Сумма имеет конечное значение, если имеется лишь конечное число констант и символов функций, что обычно и происходит.

Если задано множество R _n -арных символов отношений для каждого натурального числа n ≥ 1, то (несортированная) атомарная формула первого порядка получается применением символа n -арного отношения к n термам. Что касается функциональных символов, множество символов отношений R _n обычно непусто только при малых n . В математической логике более сложные формулы строятся из атомарных формул с использованием логических связок и квантификаторов . Например, пусть обозначим множество действительных чисел , ∀ x : x ∈ ⇒ ( x +1)⋅( x +1) ≥ 0 — математическая формула, принимающая значение «истина» в алгебре комплексных чисел . Атомарная формула называется основной, если она построена полностью из основных терминов; все основные атомарные формулы, составляемые из заданного набора функциональных и предикатных символов, составляют базу Эрбрана для этих наборов символов.

Древовидная структура черного термина-пример , с синим редексом ⁠

• Поскольку терм имеет структуру древовидной иерархии, каждому его узлу можно присвоить позицию ( путь ), то есть строку натуральных чисел, указывающую место узла в иерархии. Пустая строка, обычно обозначаемая ε, присваивается корневому узлу. Строки позиций внутри терма, выделенного черным цветом, обозначены на рисунке красным цветом.
• В каждой позиции p терма t начинается уникальный подтерм , который обычно обозначается как t | _p . Например, в позиции 122 черного терма на рисунке корень терма a + 2. Отношение «является подтермом» является частичным порядком на множестве термов; оно рефлексивно, поскольку каждый терм тривиально является подтермом самого себя.
• Термин, полученный заменой в термине t подтермина в позиции p новым термином u, обычно обозначается как t [ u ] _p . Термин t [ u ] _p также можно рассматривать как результат обобщенной конкатенации термина u с терминоподобным объектом t [.] ; последний называется контекстом или термином с дыркой (обозначенной "."; его позиция — p ), в которую , как говорят, вложен u . Например, если t — черный термин на рисунке, то t [ b +1] ₁₂ дает термин . Об этом говорит сайт https://intellect.icu . Последний термин также получается в результате встраивания термина b +1 в контекст. В неформальном смысле, операции инстанцирования и встраивания являются обратными друг другу: первая добавляет символы функций в конец терма, а вторая — в начало. Охватывающий порядок связывает терм и любой результат добавлений с обеих сторон.
• Каждому узлу терма можно присвоить его глубину (некоторые авторы называют ее высотой ), то есть расстояние (количество ребер) от корня. В этом случае глубина узла всегда равна длине его строки позиции. На рисунке уровни глубины в черном терме обозначены зеленым цветом.
• Размер термина обычно определяется количеством его узлов, или, что эквивалентно, длиной его письменного представления, включая символы без скобок. Черный и синий термины на рисунке имеют размер 15 и 5 соответственно .
• Термин u соответствует термину t , если подстановочный экземпляр u структурно равен подтерму t , или формально, если u · σ = t | _p для некоторой позиции p в t и некоторой подстановки σ. В этом случае u , t и σ называются термином-шаблоном , термином-субъектом и подстановочной подстановкой соответственно. На рисунке синий термин-шаблон ⁠ ⁠ соответствует черному подлежащему термину в позиции 1 с соответствующей заменой { x ↦ a , y ↦ a +1, z ↦ a +2}, обозначенной синими переменными, расположенными слева от их черных заменителей. Интуитивно понятно, что шаблон, за исключением переменных, должен содержаться в подлежащем; если переменная встречается в шаблоне несколько раз, в соответствующих позициях подлежащего должны быть одинаковые подтермины.
• объединяющие термины
• переписывание терминов

Когда область дискурса содержит элементы принципиально разных видов, полезно соответствующим образом разбить множество всех терминов. Для этого каждой переменной и каждому константному символу назначается сортировка (иногда также называемая типом ), а каждому функциональному символу — объявление сортировок области и сортировки диапазона. Сортированный терм f ( t 1 ,..., t n ) может быть составлен из отсортированных подтермов t ₁ ,..., t _{n ,} только если сортировка i -го подтерма совпадает с объявленной сортировкой i- го домена f . Такой терм также называется хорошо отсортированным ; любой другой терм (т. е. подчиняющийся только правилам несортировки ) называется плохо отсортированным .

Например, векторное пространство имеет связанное с ним поле скалярных чисел. Пусть W и N обозначают тип векторов и чисел соответственно, V _W и V _N — множество векторных и числовых переменных соответственно, а C _W и C _{N —} множество векторных и числовых констант соответственно. Тогда, например, и 0 ∈ C _N , а сложение векторов, скалярное умножение и скалярное произведение объявляются как ⁠ ⁠ , и ⁠ , соответственно. Предполагая переменные символы и a , b ∈ V _N , термин хорошо отсортирован, в то время какв→+ане является (поскольку + не принимает термин типа N в качестве второго аргумента). Чтобы сделать хорошо подобранный термин, дополнительное заявление ⁠ требуется. Символы функций, имеющие несколько объявлений, называются перегруженными .

Дополнительную информацию см. в разделе «Многосортная логика» , включая расширения многосортной структуры, описанные здесь.

Термины со связанными переменными

Пример обозначения	Связанные переменные	Свободные переменные	Записывается как лямбда-терм
lim н →∞ х / н	н	х	предел (λ n . div ( x , n ))
	я	н	сумма (1, n ,λ i . мощность ( i ,2))
	т	а , б , к	integral ( a , b ,λ t . sin ( k ⋅ t ))

Математические обозначения, показанные в таблице, не вписываются в схему члена первого порядка, определенную выше , поскольку все они вводят собственную локальную или связанную переменную, которая не может появляться вне области действия обозначения, например не имеет смысла. Напротив, другие переменные, называемые свободными , ведут себя как обычные переменные первого порядка, например, имеет смысл.

Все эти операторы можно рассматривать как принимающие в качестве аргумента функцию, а не значение. Например, оператор lim применяется к последовательности, то есть к отображению положительного целого числа в вещественное. Другой пример: функция C , реализующая второй пример из таблицы, Σ, будет иметь аргумент-указатель на функцию (см. врезку ниже).

Лямбда-термины могут использоваться для обозначения анонимных функций , которые будут предоставлены в качестве аргументов для lim , Σ, ∫ и т. д.

Например, квадрат функции из программы на языке C ниже можно записать анонимно как лямбда-терм λ i . i ² . Тогда общий оператор суммы Σ можно рассматривать как символ тернарной функции, принимающий значение нижней границы, значение верхней границы и функцию, которую нужно суммировать. Из-за своего последнего аргумента оператор Σ называется символом функции второго порядка . В качестве другого примера, лямбда-терм λ n . x / n обозначает функцию, которая отображает 1, 2, 3, ... в x / 1, x / 2, x / 3, ..., соответственно, то есть он обозначает последовательность ( x / 1, x / 2, x / 3, ...). Оператор lim берет такую ​​последовательность и возвращает ее предел (если определен).

В самом правом столбце таблицы показано, как каждый пример математической нотации может быть представлен лямбда-термом, а также преобразуются общие инфиксные операторы в префиксную форму.

При наличии набора V переменных символов набор лямбда-термов определяется рекурсивно следующим образом:

• каждый переменный символ x ∈ V является лямбда-термом;
• если x ∈ V — переменный символ, а t — лямбда-терм, то λ x . t также является лямбда-термом (абстракция);
• если t ₁ и t ₂ являются лямбда-термами, то ( t ₁ t ₂ ) также является лямбда-термом (приложение).

В приведенных выше мотивирующих примерах также использовались некоторые константы, такие как div , power и т. д., которые, однако, не допускаются в чистом лямбда-исчислении.

Интуитивно понятно, что абстракция λ x . t обозначает унарную функцию, которая возвращает t при заданном x , тогда как применение ( t 1 t 2 ) обозначает результат вызова функции t 1 с входными данными t 2 . Например, абстракция λ x . x обозначает функцию тождества, а λ x . y обозначает константную функцию, всегда возвращающую y . Лямбда-терм λ x .( x x ) принимает функцию x и возвращает результат применения x к себе.

• Уравнение
• Выражение (математика)
• Многосортная логика
• распределённые термины , нераспределённые термины , термины суждения ,

Исследование, описанное в статье про терм, подчеркивает ее значимость в современном мире. Надеюсь, что теперь ты понял что такое терм и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Логика