В математической логике термин обозначает математический объект , а формула обозначает математический факт. В частности, термины появляются как компоненты формулы. Это аналогично естественному языку, где именная группа относится к объекту, а целое предложение относится к факту.
Термин первого порядка рекурсивно строится из константных символов, переменных и функциональных символов . Выражение, образованное путем применения предикатного символа к соответствующему числу терминов, называется атомарной формулой , которая оценивается как истина или ложь в бивалентной логике , учитывая интерпретацию . Например, — это термин, построенный из константы 1, переменной x и бинарных функциональных символов и ; он является частью атомарной формулы , которая оценивается как истина для каждого вещественного значения x .
Помимо логики , термины играют важную роль в универсальной алгебре и системах переписывания .
При наличии набора V переменных символов, набора C постоянных символов и наборов F n символов n -арных функций, также называемых символами операторов, для каждого натурального числа n ≥ 1 набор (несортированных членов первого порядка) T рекурсивно определяется как наименьший набор со следующими свойствами: [1]
Используя интуитивную псевдограмматическую запись, это иногда записывается так:
Сигнатура термина language описывает, какие наборы символов функций F n заселены . Хорошо известными примерами являются символы унарных функций sin , cos ∈ F 1 и символы бинарных функций +, −, ⋅, / ∈ F 2 . Тернарные операции и функции с более высокой арностью возможны, но на практике встречаются редко. Многие авторы рассматривают константные символы как символы 0-арных функций F 0 , поэтому для них не требуется специального синтаксического класса.
Термин обозначает математический объект из области дискурса . Константа c обозначает именованный объект из этой области, переменная x пробегает объекты в этой области, а n -арная функция f отображает n - кортежи объектов в объекты. Например, если n ∈ V является символом переменной, 1 ∈ C является символом константы, а add ∈ F 2 является символом бинарной функции, то n ∈ T , 1 ∈ T , и (следовательно) add ( n , 1) ∈ T по первому, второму и третьему правилу построения термина соответственно. Последний термин обычно записывается как n +1, используя инфиксную нотацию и более распространенный символ оператора + для удобства.
Первоначально логики определяли термин как строку символов, соответствующую определенным правилам построения. [2] Однако, поскольку концепция дерева стала популярной в информатике, оказалось более удобным думать о термине как о дереве. Например, несколько различных строк символов, таких как " ( n ⋅( n +1))/2 ", " (( n ⋅( n +1)))/2 " и " ", обозначают один и тот же термин и соответствуют одному и тому же дереву, а именно левому дереву на рисунке выше. Отделяя древовидную структуру термина от его графического представления на бумаге, также легко учесть скобки (являющиеся только представлением, а не структурой) и невидимые операторы умножения (существующие только в структуре, а не в представлении).
Говорят, что два термина структурно , буквально или синтаксически равны, если они соответствуют одному и тому же дереву. Например, левое и правое дерево на рисунке выше являются структурно неравными терминами, хотя их можно считать « семантически равными », поскольку они всегда оцениваются в одно и то же значение в рациональной арифметике . В то время как структурное равенство можно проверить без каких-либо знаний о значении символов, семантическое равенство невозможно. Если функция /, например, интерпретируется не как рациональное, а как усечение целочисленного деления, то при n = 2 левый и правый термин оцениваются как 3 и 2 соответственно. Структурно равные термины должны согласовываться в именах своих переменных.
Напротив, термин t называется переименованием или вариантом термина u, если последний является результатом последовательного переименования всех переменных первого, т. е. если u = tσ для некоторой переименовывающей подстановки σ. В этом случае u также является переименованием t , поскольку переименовывающая подстановка σ имеет обратную σ −1 , и t = uσ −1 . Тогда оба термина также называются равными по модулю переименования . Во многих контекстах конкретные имена переменных в термине не имеют значения, например, аксиома коммутативности для сложения может быть сформулирована как 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 0 , а число символов i -арной функции как f i , число θ h различных основных членов высоты до h можно вычислить с помощью следующей рекурсивной формулы:
Если задано множество R n из n -арных символов отношений для каждого натурального числа n ≥ 1, то (несортированная первого порядка) атомарная формула получается применением n -арного символа отношения к n термам. Что касается функциональных символов, набор символов отношения R n обычно непустой только для малых n . В математической логике более сложные формулы строятся из атомарных формул с использованием логических связок и квантификаторов . Например, если обозначить множество действительных чисел , ∀ x : x ∈ ⇒ ( x +1)⋅( x +1) ≥ 0 , то это математическая формула, которая оценивается как истинная в алгебре комплексных чисел . Атомарная формула называется базовой, если она полностью построена из базовых терминов; все базовые атомарные формулы, которые можно составить из заданного набора функциональных и предикатных символов, составляют базу Эрбрана для этих наборов символов.
Когда область дискурса содержит элементы принципиально разных видов, полезно разбить набор всех терминов соответствующим образом. Для этого сортировка ( иногда также называемая типом ) назначается каждой переменной и каждому константному символу, а объявление [примечание 3] сортировок домена и сортировки диапазона — каждому функциональному символу. Сортированный термин f ( t 1 ,..., t n ) может быть составлен из отсортированных подтермов t 1 ,..., t n только в том случае, если сортировка i -го подтерма соответствует объявленной сортировке i- го домена f . Такой термин также называется хорошо отсортированным ; любой другой термин (т. е. подчиняющийся только несортированным правилам) называется плохо отсортированным .
Например, векторное пространство поставляется с соответствующим полем скалярных чисел. Пусть W и N обозначают сорт векторов и чисел соответственно, пусть V W и V N — набор векторных и числовых переменных соответственно, а C W и C N — набор векторных и числовых констант соответственно. Тогда, например , и 0 ∈ C N , а сложение векторов, скалярное умножение и скалярное произведение объявляются как , и , соответственно. Предполагая, что символы переменных и a , b ∈ V N , терм хорошо отсортирован, в то время как нет (так как + не принимает терм сорта N в качестве второго аргумента). Чтобы сделать хорошо отсортированный терм, требуется дополнительное объявление . Функциональные символы, имеющие несколько объявлений, называются перегруженными .
Более подробную информацию см. в разделе «Многосортная логика» , включая расширения многосортной структуры, описанные здесь.
Математические обозначения, показанные в таблице, не вписываются в схему термина первого порядка, как определено выше, поскольку все они вводят собственную локальную , или связанную , переменную, которая не может появляться вне области действия обозначения, например, не имеет смысла. Напротив, другие переменные, называемые свободными , ведут себя как обычные переменные термина первого порядка, например, имеет смысл.
Все эти операторы можно рассматривать как принимающие функцию, а не значение термина в качестве одного из своих аргументов. Например, оператор lim применяется к последовательности, т. е. к отображению из положительного целого числа в, например, действительные числа. В качестве другого примера, функция C для реализации второго примера из таблицы, Σ, будет иметь аргумент указателя функции (см. вставку ниже).
Лямбда-термины могут использоваться для обозначения анонимных функций , которые будут предоставлены в качестве аргументов для lim , Σ, ∫ и т. д.
Например, квадрат функции из программы на языке C ниже можно записать анонимно как лямбда-терм λ i . i 2 . Общий оператор суммы Σ тогда можно рассматривать как символ тернарной функции, принимающий нижнее граничное значение, верхнее граничное значение и функцию для суммирования. Из-за своего последнего аргумента оператор Σ называется символом функции второго порядка . В качестве другого примера, лямбда-терм λ 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 ; } При наличии набора V переменных символов набор лямбда-термов определяется рекурсивно следующим образом:
В приведенных выше мотивирующих примерах также использовались некоторые константы, такие как div , power и т. д., которые, однако, не допускаются в чистом лямбда-исчислении.
Интуитивно понятно, что абстракция λ x . t обозначает унарную функцию, которая возвращает t при заданном x , тогда как применение ( t 1 t 2 ) обозначает результат вызова функции t 1 с входными данными t 2 . Например, абстракция λ x . x обозначает функцию тождества, тогда как λ x . y обозначает константную функцию, всегда возвращающую y . Лямбда-терм λ x .( x x ) принимает функцию x и возвращает результат применения x к себе.