Замена (логика)

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

Результирующее выражение называется экземпляром подстановки или, экземпляром сокращенно, исходного выражения.

Пропозициональная логика [ править ]

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

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

(Р → С) и (Т → С)

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

П&В

и

(А ↔ А) ↔ (А ↔ А)

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

(А ↔ А)

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

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

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

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

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

е (	С	, а , г (	Икс	), и )	урожайность
е (	есть ,y)	, а , г (	С	), и )	.

Область определения dom ( σ ) замены σ обычно определяется как набор фактически замененных переменных, т.е. dom ( σ ) = { x ∈ V | хσ ≠ х }. Замена называется основной заменой, если она отображает все переменные своей области определения в основные , то есть свободные от переменных, термы. Экземпляр замены tσ основной замены является основным термином, если все находятся переменные t в σ области определения , т. е. если vars ( t ) ⊆ dom ( σ ). Замена σ называется линейной заменой, если tσ является линейным термином для некоторого (и, следовательно, каждого) линейного терма t , содержащего в точности переменные из σ области определения , т. е. с vars ( t ) = dom ( σ ). Замена σ называется плоской заменой, если xσ является переменной для каждой переменной x . Замена σ называется переименовывающей заменой, если она является перестановкой на множестве всех переменных. Как и любая перестановка, замена переименования σ всегда имеет обратную замену σ. ⁻¹, такой что tσσ ⁻¹ = т = тσ ⁻¹σ для каждого термина t . Однако невозможно определить обратную для произвольной замены.

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

Две замены считаются равными, если они отображают каждую переменную в синтаксически равные результирующие термины, формально: σ = τ , если xσ = xτ для каждой переменной x ∈ V . Композиция 1 двух замен σ = { x ₁ ↦ t ₁ , …, x _k ↦ t _k } и τ = { y ₁ ↦ u _, …, y _l ↦ u _l } получается удалением из замены { x ₁ ↦ t ₁ τ , …, x _k ↦ t _k τ , y ₁ ↦ u ₁ , …, y _l ↦ u _l } те пары y _i ↦ u _i, для которых y _i ∈ { x ₁ , …, x _k }. Композиция σ и τ обозначается στ . Композиция является ассоциативной операцией и совместима с применением замены, т. е. ( ρσ ) τ = ρ ( στ ) и ( tσ ) τ = t ( στ ) соответственно для любых замен ρ , σ , τ и каждого термина t . Тождественная замена , которая отображает каждую переменную в себя, является нейтральным элементом композиции замены. Замена σ называется идемпотентной , если σσ = σ и, следовательно, tσσ = tσ для каждого терма t . Когда x _i ≠ t _i для всех i , замена { x ₁ ↦ t ₁ , …, x _k ↦ t _k } является идемпотентной тогда и только тогда, когда ни одна из переменных x _i не встречается ни в одном t _j . Композиция замещения не коммутативна, т. е. σ может отличаться от τ , даже если σ и τ идемпотентны. ^[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 ↦ z } = { x ↦ z , y ↦ z }, но { y ↦ z } { x ↦ y } = { x ↦ y , y ↦ z } .

Алгебра [ править ]

Замена — основная операция в алгебре , в частности в компьютерной алгебре . ^[4]^[5]

Обычный случай замены включает в себя полиномы , где замена числового значения (или другого выражения) на неопределенное одномерное многочлен равнозначно оценке многочлена по этому значению. Действительно, эта операция происходит настолько часто, что к ней часто адаптируются обозначения многочленов; вместо того, чтобы обозначать многочлен именем типа P , как это можно было бы сделать для других математических объектов, можно было бы определить

P(X)=X^{5}-3X^{2}+5X-17

так что замену X можно обозначить заменой внутри « P ( X )», скажем

P(2)=13

или

P(X+1)=X^{5}+5X^{4}+10X^{3}+7X^{2}+4X-14.

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

Замена связана с композицией функций , но не идентична ей ; оно тесно связано с β -редукцией в лямбда-исчислении . Однако в отличие от этих понятий акцент в алгебре делается на сохранении алгебраической структуры посредством операции подстановки, т. е. на том факте, что замена дает гомоморфизм рассматриваемой структуры (в случае многочленов - кольцевой структуры). ^{[ нужна цитата ]}

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

Примечания [ править ]

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

Цитаты [ править ]

^ Перейти обратно: ^а ^б Дэвид А. Даффи (1991). Принципы автоматического доказательства теорем . Уайли.
^ Перейти обратно: ^а ^б Франц Баадер , Уэйн Снайдер (2001). Алан Робинсон и Андрей Воронков (ред.). Теория объединения (PDF) . Эльзевир. стр. 439–526. Архивировано из оригинала (PDF) 8 июня 2015 г. Проверено 24 сентября 2014 г.
^ Н. Дершовиц; Ж.-П. Жуанно (1990). «Переписать системы». . Ян ван Леувен (ред.) Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 243–320.
^ Маргарет Х. Хофт; Хартмут Ф.В. Хофт (6 ноября 2002 г.). Вычисления с помощью Mathematica . Эльзевир. ISBN 978-0-08-048855-4 .
^ Андре Хек (6 декабря 2012 г.). Знакомство с Мэйпл . Springer Science & Business Media. ISBN 978-1-4684-0484-5 . замена.

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

Краббе, М. (2004). О понятии замены . Логический журнал IGPL, 12, 111–124.
Карри, Х.Б. (1952) Об определении замены, замены и родственных понятий в абстрактной формальной системе . Философское обозрение Лувена 50, 251–269.
Хантер, Г. (1971). Металогика: введение в метатеорию стандартной логики первого порядка . Издательство Калифорнийского университета. ISBN 0-520-01822-2
Клини, Южная Каролина (1967). Математическая логика . Перепечатано в 2002 г., Дувр. ISBN 0-486-42533-9

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

Замена в n Lab

[4] Некоторые авторы используют [ t ₁ / x ₁ , …, t _k / x _k ] для обозначения этой замены, например М. Вирсинг (1990). Ян ван Леувен (ред.). Алгебраическая спецификация . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 675–788. , здесь: с. 682.

[5] С алгебры термов точки зрения , множество термов T является алгеброй свободных термов над множеством V переменных, следовательно, для каждого отображения подстановки σ: V → T существует уникальный гомоморфизм σ : T → T , который согласуется с σ на V ⊆ Т ; определенное выше применение σ к терму t тогда рассматривается как применение функции σ к аргументу t .

[Duffy.1991-1] Перейти обратно: ^а ^б Дэвид А. Даффи (1991). Принципы автоматического доказательства теорем . Уайли.

[Baader.Snyder.2001-2] Перейти обратно: ^а ^б Франц Баадер , Уэйн Снайдер (2001). Алан Робинсон и Андрей Воронков (ред.). Теория объединения (PDF) . Эльзевир. стр. 439–526. Архивировано из оригинала (PDF) 8 июня 2015 г. Проверено 24 сентября 2014 г.

[Dershowitz.Jouannaud.1990-3] Н. Дершовиц; Ж.-П. Жуанно (1990). «Переписать системы». . Ян ван Леувен (ред.) Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 243–320.

[HoftHoft2002-6] Маргарет Х. Хофт; Хартмут Ф.В. Хофт (6 ноября 2002 г.). Вычисления с помощью Mathematica . Эльзевир. ISBN 978-0-08-048855-4 .

[HECK2012-7] Андре Хек (6 декабря 2012 г.). Знакомство с Мэйпл . Springer Science & Business Media. ISBN 978-1-4684-0484-5 . замена.

[1]

[2]

[3]

[примечание 1]

[заметка 2]

[4]

[5]