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

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

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

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

Формальное определение

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

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

• каждый переменный символ является термом: V ⊆ T ,
• каждый постоянный символ является термом: C ⊆ T ,
• из каждых n термов t ₁ ,..., t _n и каждого n -арного функционального символа f ∈ F _n больший терм 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, используя для удобства инфиксную запись и более распространенный символ оператора +.

структура

Первоначально логики определяли термин как строку символов , соответствующую определенным правилам построения. Однако, поскольку концепция дерева стала популярной в информатике, оказалось удобнее думать о таком термине как о дереве. Например, несколько отдельных строк символов, например " ( n ⋅( n +1))/2 ", " (( n ⋅( n +1)))/2 " и " ${\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 не является допустимой версией аксиомы коммутативности.

Наземные и линейные термины

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

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

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

• θ ₀ = f ₀ , поскольку основной член высоты 0 может быть только константой,
• $\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 . В математической логике более сложные формулы строятся из атомарных формул с использованием логических связок и кванторов . Например, позволив $\mathbb {R}$ обозначаем множество действительных чисел , ∀ x : x ∈ $\mathbb {R}$⇒ ( x +1)⋅( x +1) ≥ 0 — математическая формула, имеющая истинное значение в алгебре комплексных чисел . Атомная формула называется основной, если она полностью построена из основных членов; все основные атомарные формулы, которые можно составить из заданного набора символов функций и предикатов, составляют основу Эрбрана для этих наборов символов.

Операции с терминами

Древовидная структура термина черного примера ${\frac {a*((a+1)*(a+2))}{1*(2*3)}}$, с синим редексом $x*(y*z)$

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

Связанные понятия

Сортированные термины

Основная статья: Многосортная логика

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

Например, векторное пространство имеет связанное с ним поле скалярных чисел. Пусть W и N обозначают сорт векторов и чисел соответственно, пусть V _W и V _N — набор векторных и числовых переменных соответственно, а C _W и CN _— набор векторных и числовых констант соответственно. Тогда, например ${\vec {0}}\in C_{W}$ и 0 ∈ CN _, а сложение векторов, скалярное умножение и скалярное произведение объявляются как $+:W\times W\to W,*:W\times N\to W$, и $\langle .,.\rangle :W\times W\to N$, соответственно. Предполагая переменные символы ${\vec {v}},{\vec {w}}\in V_{W}$ и a , b ∈ V _N , термин $\langle ({\vec {v}}+{\vec {0}})*a,{\vec {w}}*b\rangle$ хорошо отсортирован, в то время как ${\vec {v}}+a$нет (поскольку + не принимает термин типа N в качестве второго аргумента). Для того, чтобы $a*{\vec {v}}$ хорошо отсортированный термин, дополнительное объявление $*:N\times W\to W$требуется. Функциональные символы, имеющие несколько объявлений, называются перегруженными .

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

Лямбда-термины

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

Обозначения пример	Граница переменные	Бесплатно переменные	Написано как лямбда-терм
lim n →∞ x / n	н	Икс	предел (λ n . div ( x , n ))
$\sum _{i=1}^{n}i^{2}$	я	н	сумма (1, n , λ i . степень ( i ,2))
$\int _{a}^{b}\sin(k\cdot t)dt$	т	а , б , к	интеграл ( а , б , λ т . грех ( k ⋅ т ))

Основная статья: Лямбда-терм

Мотивация

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

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

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

Например, квадрат функции из приведенной ниже программы на языке C можно записать анонимно как лямбда-терм λ i . я ² . Тогда общий оператор суммы Σ можно рассматривать как символ троичной функции, принимающий значение нижней границы, значение верхней границы и функцию, подлежащую суммированию. Благодаря последнему аргументу оператор Σ называется функциональным символом второго порядка . Другой пример: лямбда-терм λ n . x / n обозначает функцию, которая отображает 1, 2, 3,... в x /1, x /2, x /3,... соответственно, то есть обозначает последовательность ( x / 1, x / 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  ); 
      вернуть   разрешение  ; 
  } 

 Int   Square  (  int   i  )   {   return   i  *  i  ;    }              // реализует анонимную функцию (лямбда i. i*i);   однако C требует для него имя 

 #include   <stdio.h> 
 int   main  (  void  )   { 
     int   n  ; 
      scanf  (  "%d"  ,  &  n  ); 
      printf  (  "%d  \n  "  ,   сумма  (  1  ,   n  ,   квадрат  ));           // применяет оператор суммы для суммирования квадратов 
     return   0  ; 
  } 

Определение

Учитывая набор 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). Переписывание терминов и все такое . Издательство Кембриджского университета. стр. 1–2 и 34–35. ISBN  978-0-521-77920-3 .