Замена — это синтаксическое преобразование формальных выражений. Применить замену к выражению означает последовательно заменить символы его переменной или заполнителя другими выражениями.
Результирующее выражение называется экземпляром подстановки или, сокращенно, экземпляром исходного выражения.
Если ψ и φ представляют собой формулы пропозициональной логики , ψ является примером замены φ тогда и только тогда, когда ψ может быть получено из φ путем подстановки формул для пропозициональных переменных в φ , заменяя каждое вхождение одной и той же переменной вхождением той же формулы . . Например:
является экземпляром замены:
и
является экземпляром замены:
В некоторых системах вывода для логики высказываний новое выражение ( предложение ) может быть введено в строку вывода, если оно является экземпляром замены предыдущей строки вывода (Hunter 1971, стр. 118). Именно так вводятся новые строки в некоторых аксиоматических системах . В системах, использующих правила преобразования , правило может включать использование экземпляра подстановки с целью введения определенных переменных в вывод.
Пропозициональная формула является тавтологией , если она истинна при любой оценке (или интерпретации ) ее символов-предикатов. Если Φ — тавтология, а Θ — экземпляр подстановки Φ, то Θ снова является тавтологией. Этот факт подразумевает обоснованность правила вывода, описанного в предыдущем разделе.
В логике первого порядка подстановкой называется полное отображение σ : V → T переменных в термины ; многие, [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 и любой другой переменной. самому себе; x i должен быть попарно различен. Применение этой замены к термину 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 ) } к термину
Область определения dom ( σ ) замены σ обычно определяется как набор фактически замененных переменных, т.е. dom ( σ ) = { x ∈ V | хσ ≠ х }. Замена называется основной заменой, если она отображает все переменные своей области определения в основные , то есть свободные от переменных, термы. Экземпляр замены tσ основной замены является основным термином, если все переменные t находятся в области определения σ , т. е. если vars ( t ) ⊆ dom ( σ ). Замена σ называется линейной заменой, если tσ является линейным термином для некоторого (и, следовательно, каждого) линейного термина t , содержащего в точности переменные из области определения σ , т. е. с vars ( t ) = dom ( σ ). Замена σ называется плоской заменой, если 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 } одновременно линейно и Flat, но не переименование, поскольку оно отображает и 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 ↦ 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 . Композиция двух замен σ = { x 1 ↦ t 1 , …, x k ↦ t k } и τ = { y 1 ↦ u 1 , …, y l ↦ u l } получается удалением из замены { 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 i ≠ t i для всех i , замена { x 1 ↦ t 1 , …, 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 , как это можно было бы сделать для других математических объектов, можно было бы определить
так что замену X можно обозначить заменой внутри « P ( X )», скажем
или
Замену можно применять и к другим видам формальных объектов, построенных из символов, например к элементам свободных групп . Чтобы определить замену, нужна алгебраическая структура с соответствующим универсальным свойством , которая утверждает существование уникальных гомоморфизмов, которые переводят неопределенные значения в определенные значения; тогда замена сводится к нахождению образа элемента при таком гомоморфизме.
Замена связана с композицией функций , но не идентична ей ; оно тесно связано с β -редукцией в лямбда-исчислении . Однако в отличие от этих понятий акцент в алгебре делается на сохранении алгебраической структуры посредством операции подстановки, т. е. на том факте, что замена дает гомоморфизм рассматриваемой структуры (в случае многочленов - кольцевой структуры). [ нужна цитата ]
замена.
