Замена (логика)
Замена синтаксическое это — преобразование формальных выражений.Применить означает последовательно заменить символы его переменной замену к выражению или заполнителя другими выражениями.
Результирующее выражение называется экземпляром подстановки или, экземпляром сокращенно, исходного выражения.
Пропозициональная логика
[ редактировать ]Определение
[ редактировать ]Если ψ и φ представляют собой формулы пропозициональной логики , ψ является примером замены φ φ тогда и только тогда, когда ψ может быть получено из пропозициональных путем подстановки формул для переменных в φ , заменяя каждое вхождение одной и той же переменной вхождением той же формулы. . Например:
- (Р → С) и (Т → С)
является экземпляром замены:
- П&В
и
- (А ↔ А) ↔ (А ↔ А)
является экземпляром замены:
- (А ↔ А)
В некоторых системах вывода для логики высказываний новое выражение ( предложение ) может быть введено в строку вывода, если оно является экземпляром замены предыдущей строки вывода (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 ) } к термину
е ( С , а , г ( х ), и ) урожайность е ( есть ,y) , а , г ( С ), и ) .
Область определения dom ( σ ) замены σ обычно определяется как набор фактически замененных переменных, т.е. dom ( σ ) = { x ∈ V | хσ ≠ х }.Замена называется основной заменой, если она отображает все переменные своей области определения в основные , то есть свободные от переменных, термы.Экземпляр замены tσ основной замены является основным термином, если все t переменные находятся в σ области определения , т. е. если vars ( t ) ⊆ dom ( σ ).Замена σ называется линейной заменой, если tσ является линейным термином для некоторого (и, следовательно, каждого) линейного термина t, содержащего в точности переменные из σ области определения , т. е. с vars ( t ) = dom ( σ ).Замена σ называется плоской заменой, если xσ является переменной для каждой переменной x .Замена σ называется переименовывающей заменой, если она является перестановкой на множестве всех переменных. Как и любая перестановка, замена переименования σ всегда имеет обратную замену σ. −1 , такой что tσσ −1 = т = тσ −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 ↦ 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 1 ↦ t 1 , …, x k ↦ t k } и τ = { y 1 ↦ u x , …, y l ↦ u l } получается удалением из замены { 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 )», скажем
или
Замену можно также применять к другим видам формальных объектов, построенных из символов, например к элементам свободных групп . Чтобы определить замену, нужна алгебраическая структура с соответствующим универсальным свойством , которая утверждает существование уникальных гомоморфизмов, которые переводят неопределенные значения в определенные значения; тогда замена сводится к нахождению образа элемента при таком гомоморфизме.
Замена связана с композицией функций , но не идентична ей ; оно тесно связано с β -редукцией в лямбда-исчислении . Однако в отличие от этих понятий акцент в алгебре делается на сохранении алгебраической структуры посредством операции подстановки, т. е. на том факте, что замена дает гомоморфизм рассматриваемой структуры (в случае многочленов - кольцевой структуры). [ нужна ссылка ]
См. также
[ редактировать ]- Интегрирование путем замены
- Лямбда-исчисление § Замена
- Строковая интерполяция
- Свойство замены равенства
- Тригонометрическая замена
- Универсальная реализация
Примечания
[ редактировать ]- ^ Некоторые авторы используют [ t 1 / x 1 , …, t k / x k ] для обозначения этой замены, например М. Вирсинг (1990). Ян ван Леувен (ред.). Алгебраическая спецификация . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 675–788. , здесь: с. 682.
- ^ С алгебры термов точки зрения T , множество термов является алгеброй свободных термов над множеством V переменных, следовательно, для каждого отображения подстановки σ: V → T существует уникальный гомоморфизм σ : T → T , который согласуется с σ на V ⊆ Т ; определенное выше применение σ к терму t тогда рассматривается как применение функции σ к аргументу t .
Цитаты
[ редактировать ]- ^ Jump up to: а б Дэвид А. Даффи (1991). Принципы автоматического доказательства теорем . Уайли.
- ^ Jump up to: а б Франц Баадер , Уэйн Снайдер (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
