В математической логике термин обозначает математический объект, а формула обозначает математический факт. В частности, термины появляются как компоненты формулы. Это аналогично естественному языку, где именная фраза относится к объекту, а целое предложение относится к факту.
A терм первого порядка - это рекурсивно построенный из постоянных символов, переменных и функциональных символов. Выражение, сформированное путем применения символа предиката к соответствующему количеству терминов, называется атомарной формулой , которая принимает значение истина или ложь. в бивалентной логике, учитывая интерпретацию. Например, - это член, построенный из константы 1, переменной x и двоичные функциональные символы и ; это часть атомарной формулы , которая оценивается как истина для каждого вещественного значения x.
Помимо логики, термины играют важную роль в универсальной алгебре и системах переписывания.
Для данного набора V переменных символов, набора C постоянных символов и набора F n n-арных функциональных символов, также называемых символами операторов, для для каждого натурального числа n ≥ 1 набор (неотсортированных) термов первого порядка T рекурсивно определен как наименьший набор со следующими свойствами:
Используя интуитивно понятный, псевдо- грамматическая нотация, иногда это записывается как: t :: = x | c | f (t 1,..., t n). Обычно заселяются только первые несколько наборов функциональных символов 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 с использованием инфиксной записи и более распространенного символа оператора + для удобства.
Первоначально логики определяли термин как строку символов, придерживающуюся определенных строительных правил. Однако, поскольку концепция дерева стала популярной в компьютерных науках, оказалось, что удобнее рассматривать термин как дерево. Например, несколько отдельных строк символов, например «(n⋅ (n + 1)) / 2», «((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 не является допустимой версией аксиомы коммутативности.
Набор переменных терма 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 - это математическая формула, истинная в алгебре комплексные числа. Атомарная формула называется основной, если она полностью построена на основных терминах; все основные атомарные формулы, составленные из заданного набора символов функций и предикатов, составляют базу Хербрана для этих наборов символов.
Когда область дискурса содержит элементы принципиально разного типа, полезно соответственно разделить набор всех терминов. С этой целью каждой переменной и каждому константному символу присваивается sort (иногда также называемый type ), а каждому функциональному символу присваивается объявление сортировки по домену и сортировки по диапазону. отсортированный термин 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 в качестве второго аргумента). Чтобы сделать хорошо отсортированным термином, необходимо дополнительное объявление является обязательным. Функциональные символы, имеющие несколько объявлений, называются перегруженными .
См. многосортную логику для получения дополнительной информации, включая расширения многосортной структуры, описанной здесь.
Обозначение. пример | Связанные. переменные | Свободные. переменные | Записывается как. лямбда-член |
---|---|---|---|
limn → ∞ x / n | n | x | предел (λn. Div (x, n)) |
i | n | сумма (1, n, λi. Степень (i, 2)) | |
t | a, b, k | интеграл (a, b, λt. sin (k⋅t)) |
Математические обозначения, показанные в таблице, не вписываются в схему члена первого порядка, как определено выше, поскольку все они вводят собственный локальный или bound, переменная, которая не может появляться за пределами области нотации, например не не имеет смысла. Напротив, другие переменные, называемые free, ведут себя как обычные термальные переменные первого порядка, например делает имеет смысл.
Все эти операторы можно рассматривать как принимающие функцию, а не член значения в качестве одного из своих аргументов. Например, оператор lim применяется к последовательности, то есть к отображению положительного целого числа на, например, вещественные числа. В качестве другого примера, функция C для реализации второго примера из таблицы, ∑, будет иметь аргумент указателя функции (см. Рамку ниже).
Лямбда-термины могут использоваться для обозначения анонимных функций, которые должны быть предоставлены в качестве аргументов для lim, ∑, ∫ и т. Д.
Например, функция square из приведенной ниже программы на языке C может быть анонимно записана как лямбда-член λi. я. Затем общий оператор суммы ∑ можно рассматривать как троичный функциональный символ, принимающий значение нижней границы, значение верхней границы и функцию, которая должна быть суммирована. Из-за последнего аргумента оператор ∑ называется символом функции второго порядка . Другой пример - лямбда-член λn. x / n обозначает функцию, которая отображает 1, 2, 3,... в x / 1, x / 2, x / 3,..., соответственно, то есть обозначает последовательность ( х / 1, х / 2, х / 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; } // implements anonymous function (lambda i. i*i); however, C requires a name for it #includeint main (void) {int n; scanf ("% d", n); printf ("% d \ n", sum (1, n, square)); / / применяет оператор суммы для суммирования квадратов return 0;}