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

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

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

Пропозициональная логика

Определение

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

(Р → С) и (Т → С)

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

П&В

и

(А ↔ А) ↔ (А ↔ А)

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

(А ↔ А)

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

Тавтологии

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

Логика первого порядка

В первого порядка подстановкой ; называется полное σ : V → T переменных логике в термины отображение много, но не все авторы дополнительно требуют σ ( x ) = x , кроме конечного числа для всех переменных x . Обозначение { x ₁ ↦ t ₁ , …, x _k ↦ t _k } относится к замене, отображающей каждую переменную x _i в соответствующий термин t _i , для i =1,…, k и каждую другую переменную в себя; x . _i должен быть попарно различен Применение этой замены к термину t записывается в постфиксной записи как t { x ₁ ↦ t ₁ , ..., x _k ↦ t _k }; это означает (одновременно) заменить каждое вхождение каждого x _i в t на t _i . Результат tσ применения замены σ к термину t называется экземпляром этого термина t . Например, применив замену { x ↦ z , z ↦ h ( a , 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 _x , …, y _l ↦ u _l } получается удалением из замены { ₁ ↦ 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 . Композиция замещения не коммутативна, т. е. σ может отличаться от τ , даже если σ и τ идемпотентны.

Например, { 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 } .

Алгебра

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

Обычный случай замены включает в себя полиномы , где замена числового значения (или другого выражения) на неопределенное одномерное многочлен равнозначно оценке многочлена по этому значению. Действительно, эта операция происходит настолько часто, что к ней часто адаптируются обозначения многочленов; вместо того, чтобы обозначать полином именем типа 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.$

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

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

См. также

• Интегрирование путем замены
• Лямбда-исчисление § Замена
• Строковая интерполяция
• Свойство замены равенства
• Тригонометрическая замена
• Универсальная реализация

Ссылки

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

Внешние ссылки

• Замена в n Lab