Из Википедии, бесплатной энциклопедии
  (Перенаправлено из наземного экземпляра )
Перейти к навигации Перейти к поиску

Подстановка - фундаментальное понятие в логике . Замещение является синтаксическим преобразованием в формальных выражениях. Чтобы применить подстановку к экспрессии средства , чтобы последовательно заменить его переменной, или заполнитель, символы другими выражениями. Результирующее выражение называется экземпляром подстановки или коротким экземпляром исходного выражения.

Логика высказываний [ править ]

Определение [ править ]

Там , где ψ и ф представляют формулы логики высказываний, ψ является замена экземпляра из ф тогда и только тогда , когда ψ могут быть получены из ф путем подстановки формулы для символов в ф , заменяя каждое вхождение одного и того же символа путем вхождения той же формулы. Например:

(R → S) и (T → S)

является экземпляром подстановки:

P&Q

а также

(А ↔ А) ↔ (А ↔ А)

является экземпляром подстановки:

(А ↔ А)

В некоторых системах дедукции для логики высказываний новое выражение ( пропозиция ) может быть введено в строку вывода, если оно является экземпляром подстановки предыдущей строки вывода (Hunter 1971, стр. 118). Так вводятся новые линии в некоторых аксиоматических системах . В системах, использующих правила преобразования , правило может включать использование экземпляра подстановки с целью введения определенных переменных в производную.

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

Тавтологии [ править ]

Пропозициональная формула является тавтологией, если она истинна при любой оценке (или интерпретации ) ее предикатных символов. Если Φ - тавтология, а Θ - подстановка Φ, то Θ снова является тавтологией. Этот факт подразумевает обоснованность правила дедукции, описанного в предыдущем разделе. [ необходима цитата ]

Логика первого порядка [ править ]

В логике первого порядка , А замена является полным отображением σ : V → T из переменных в терминах ; many, [1] : 73 [2] : 445 но не все [3] : 250 авторов дополнительно требуют σ ( x ) = x для всех переменных x, кроме конечного числа . Обозначение { x 1  ↦  t 1 ,…, x k  ↦  t k }[примечание 1] относится к замене, отображающей каждую переменную x i в соответствующий терм t i , для i = 1,…, k , и каждую другую переменную в себя; х я должен быть попарно различны. Применение этой замены к терму t записывается в постфиксной записи как t { x 1  ↦  t 1 , ..., x k  ↦  t k }; это означает (одновременно) заменить каждое вхождение каждого x i в tпользователя t i . [примечание 2] Результат tσ применения подстановки σ к члену t называется экземпляром этого члена t . Например, применяя замену { x  ↦  z , z  ↦  h ( a , y )} к члену

f (z, а , г (Икс), у )  дает
f (ч ( а , у ), а , г (z), у ).

Область определения dom ( σ ) подстановки σ обычно определяется как набор фактически заменяемых переменных, т. Е. Dom ( σ ) = { x ∈ V | xσ ≠ x }. Подстановка называется основной заменой, если она отображает все переменные своего домена на основные , т.е. без переменных, термины. Экземпляр замены tσ подстановки земли являются термами , если все т « ы переменных в сге » ы области, то есть , если вары ( т ) ⊆dom ( σ ). Подстановка σ называется линейное замещение , если tσ является линейным термином для некоторого (и , следовательно , каждый) линейный член т , содержащий именно переменные сг ' ы домена, т.е. с VARS ( т ) = дом ( сг ). Подстановка σ называется плоской заменой, если xσ является переменной для каждой переменной x . Подстановка σ называется подстановкой переименования, если это перестановкана множестве всех переменных. Как и любая перестановка, переименование σ всегда имеет обратную замену σ −1 , такую ​​что tσσ −1 = t = tσ −1 σ для каждого члена t . Однако невозможно определить обратное для произвольной замены.

Например, { x  ↦ 2, y  ↦ 3 + 4} является основной заменой, { x  ↦  x 1 , y  ↦  y 2 +4} не является основной и неплоской, но линейной, { x  ↦  y 2 , y  ↦  y 2 +4} является нелинейным и неплоским, { x  ↦  y 2 , y  ↦  y 2 } является плоским, но нелинейным, { x  ↦  x 1 , y  ↦  y 2} одновременно является линейным и плоским, но не является переименованием, поскольку он отображает y и y 2 в y 2 ; каждая из этих замен имеет набор { x , y } в качестве области определения. Пример подстановки переименования: { x  ↦  x 1 , x 1  ↦  y , y  ↦  y 2 , y 2  ↦  x }, он имеет обратное { x  ↦  y 2 , y 2  ↦  y , y  ↦ x 1 , x 1  ↦  x }. Плоская подстановка { x  ↦  z , y  ↦  z } не может иметь обратного, так как, например, ( x + y ) { x  ↦  z , y  ↦  z } = z + z , и последний член не может быть преобразован обратно в x + y , поскольку информация о происхождении z теряется. Замена основания { x ↦ 2} не может иметь инверсию из-за аналогичной потери исходной информации, например, в ( x +2) { x  ↦ 2} = 2 + 2, даже если замена констант на переменные была разрешена каким-то фиктивным видом «обобщенных замен».

Две замены считаются равными , если они отображают каждую переменную в структурно равных условиях результата, формально: σ = τ , если xσ = хт для каждой переменной х ∈ V . Композицию из двух замен σ = { х 1  ↦  т 1 , ..., х к  ↦  т к } и τ = { у 1  ↦  U 1 , ..., у л  ↦ U л} получается удалением из подстановки { x 1  ↦  t 1 τ ,…, x k  ↦  t k τ , y 1  ↦  u 1 ,…, y l  ↦  u l } тех пар y i  ↦  u i, для которых y i ∈ { x 1 ,…, x k }. Композиция σ и τ обозначается στ. Композиция является ассоциативной операцией и совместима с применением замены, т. Е. ( Ρσ ) τ = ρ ( στ ) и ( tσ ) τ = t ( στ ), соответственно, для каждой замены ρ , σ , τ и каждого члена t . Замена идентичности , которая отображает каждую переменную в себе, является нейтральным элементом замещения композиции. Подстановка σ называется идемпотентной, если σσ = σ , и, следовательно, tσσ =tσ для каждого члена t . Подстановка { x 1  ↦  t 1 ,…, x k  ↦  t k } идемпотентна тогда и только тогда, когда ни одна из переменных x i не встречается ни в одном t i . Подстановочная композиция не коммутативна, то есть στ может отличаться от τσ, даже если σ и τ идемпотентны. [1] : 73–74 [2] : 445–446

Например, { x  ↦ 2, y  ↦ 3 + 4} равно { y  ↦ 3 + 4, x  ↦ 2}, но отличается от { x  ↦ 2, y  ↦ 7}. Подстановка { x  ↦  y + y } идемпотентна, например (( x + y ) { x ↦ y + y }) { x ↦ y + y } = (( y + y ) + y ) { x ↦ y + y } = ( y + y) + y , тогда как подстановка { x  ↦  x + y } неидемпотентна, например (( x + y ) { x ↦ x + y }) { x ↦ x + y } = (( x + y ) + y ) { х ↦ х + у } = (( х + у ) + у ) + у . Пример некоммутирующих замен: { x  ↦  y } { y  ↦ г } = { х  ↦  г , у  ↦  г }, а { у  ↦  г } { х  ↦  у } = { х  ↦  у , у  ↦  г }.

См. Также [ править ]

Заметки [ править ]

  1. ^ некоторые авторы используют [ t 1 / x 1 ,…, t k / x k ] для обозначения этой замены, например M. Wirsing (1990). Ян ван Леувен (ред.). Алгебраическая спецификация . Справочник по теоретической информатике. B . Эльзевир. С. 675–788., здесь: стр. 682;
  2. ^ Сточки зрения термальной алгебры , множествотермов T является алгеброй свободных термов над множествомпеременных V , следовательно, для каждого отображения подстановки σ: V → T существует единственный гомоморфизм σ : T → T, который согласуется с σ на V ⊆ T ; определенное выше применение σ к члену t затем рассматривается как применение функции σ к аргументу t .

Ссылки [ править ]

  • Краббе, М. (2004). О понятии замещения . Логический журнал ИГПЛ, 12, 111–124.
  • Карри, HB (1952) Об определении подстановки, замены и родственных понятий в абстрактной формальной системе . Философское ревю де Лувен 50, 251–269.
  • Хантер, Г. (1971). Металогика: Введение в метатеорию стандартной логики первого порядка . Калифорнийский университет Press. ISBN 0-520-01822-2 
  • Клини, SC (1967). Математическая логика . Перепечатано в 2002 г., Дувр. ISBN 0-486-42533-9 
  1. ^ а б Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем . Вайли.
  2. ^ a b Франц Баадер , Уэйн Снайдер (2001). Алан Робинсон и Андрей Воронков (ред.). Теория объединения (PDF) . Эльзевир. С. 439–526.
  3. ^ Н. Дершовиц; Ж.-П. Жуанно (1990). «Системы перезаписи». В Яне ван Леувене (ред.). Формальные модели и семантика . Справочник по теоретической информатике. B . Эльзевир. С. 243–320.

Внешние ссылки [ править ]

  • Замена в nLab