Термин (логика)

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

Термин первого порядка рекурсивно строится из константных символов, переменных и функциональных символов . Выражение, образованное путем применения предикатного символа к соответствующему числу терминов, называется атомарной формулой , которая оценивается как истина или ложь в бивалентной логике , учитывая интерпретацию . Например, ⁠ ⁠${\displaystyle (x+1)*(x+1)}$ — это термин, построенный из константы 1, переменной x и бинарных функциональных символов ⁠ ⁠${\displaystyle +}$ и ⁠ ⁠${\displaystyle *}$ ; он является частью атомарной формулы ⁠ ⁠,${\displaystyle (x+1)*(x+1)\geq 0}$ которая оценивается как истина для каждого вещественного значения x .

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

При наличии набора 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 ).

Сигнатура термина language описывает, какие наборы символов функций 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 ⋅( n +1))/2 ", " (( n ⋅( n +1)))/2 " и " ", обозначают один и тот же термин и соответствуют одному и тому же дереву, а именно левому дереву на рисунке выше. Отделяя древовидную структуру термина от его графического представления на бумаге, также легко учесть скобки (являющиеся только представлением, а не структурой) и невидимые операторы умножения (существующие только в структуре, а не в представлении).${\displaystyle {\frac {n(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 не является допустимой версией аксиомы коммутативности. ^{[примечание 1] [примечание 2]}

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

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

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

• θ ₀ = f ₀ , поскольку основной член высоты 0 может быть только константой,
• ${\displaystyle \theta _{h+1}=\sum _{i=0}^{\infty }f_{i}\cdot \theta _{h}^{i}}$, поскольку основной член высоты до h +1 может быть получен путем составления любых i основных членов высоты до h , используя символ функции корня i . Сумма имеет конечное значение, если имеется только конечное число констант и символов функций, что обычно и бывает.

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

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

Когда область дискурса содержит элементы принципиально разных видов, полезно разбить набор всех терминов соответствующим образом. Для этого сортировка ( иногда также называемая типом ) назначается каждой переменной и каждому константному символу, а объявление ^{[примечание 3]} сортировок домена и сортировки диапазона — каждому функциональному символу. Сортированный термин f ( t ₁ ,..., 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 в качестве второго аргумента). Чтобы сделать хорошо отсортированный терм, требуется дополнительное объявление ⁠ ⁠ . Функциональные символы, имеющие несколько объявлений, называются перегруженными .${\displaystyle {\vec {0}}\in C_{W}}$${\displaystyle +:W\times W\to W, *:W\times N\to W}$${\displaystyle \langle .,.\rangle :W\times W\to N}$${\displaystyle {\vec {v}},{\vec {w}}\in V_{W}}$${\displaystyle \langle ({\vec {v}}+{\vec {0}})*a, {\vec {w}}*b\rangle }$${\displaystyle {\vec {v}}+a}$${\displaystyle a*{\vec {v}}}$${\displaystyle *:N\times W\to W}$

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

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

Пример записи	Связанные переменные	Свободные переменные	Записывается как лямбда-терм
лимн →∞ х / н	н	х	предел (λ n . div ( x , n ))
${\displaystyle \sum _{i=1}^{n}i^{2}}$	я	н	сумма (1, n ,λ i . мощность ( i ,2))
${\displaystyle \int _{a}^{b}\sin(k\cdot t)dt}$	т	а , б , к	интеграл ( a , b , λt.sin ( k⋅t ) ) ​​​

Математические обозначения, показанные в таблице, не вписываются в схему термина первого порядка, как определено выше, поскольку все они вводят собственную локальную , или связанную , переменную, которая не может появляться вне области действия обозначения, например, не имеет смысла. Напротив, другие переменные, называемые свободными , ведут себя как обычные переменные термина первого порядка, например, имеет смысл.${\displaystyle t\cdot \int _{a}^{b}\sin(k\cdot t)\;dt}$${\displaystyle k\cdot \int _{a}^{b}\sin(k\cdot t)\;dt}$

Все эти операторы можно рассматривать как принимающие функцию, а не значение термина в качестве одного из своих аргументов. Например, оператор 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 принимает такую ​​последовательность и возвращает ее предел (если определен).

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

int sum ( int lwb , int upb , int fct ( int )) { // реализует общий оператор суммы int res = 0 ; for ( int i = lwb ; i <= upb ; ++ i ) res += fct ( i ); return res ; }                      int square ( int i ) { return i * i ; } // реализует анонимную функцию (lambda i. i*i); однако C требует для нее имени       #include <stdio.h> int main ( void ) { int n ; scanf ( " %d " , & n ); printf ( " %d \n " , sum ( 1 , n , square )); // применяет оператор суммы для суммирования квадратов return 0 ; }             

This section needs expansion. You can help by adding to it. (April 2021)

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

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

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

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

• Уравнение
• Выражение (математика)

• Франц Баадер ; Тобиас Нипков (1999). Переписывание терминов и все такое . Cambridge University Press. С. 1–2 и 34–35. ISBN 978-0-521-77920-3.