stringtranslate.com

Sustitución (lógica)

Una sustitución es una transformación sintáctica de expresiones formales . Aplicar una sustitución a una expresión significa reemplazar consistentemente sus símbolos variables o marcadores de posición con otras expresiones .

La expresión resultante se denomina instancia de sustitución , o instancia para abreviar, de la expresión original.

Lógica proposicional

Definición

Donde ψ y φ representan fórmulas de lógica proposicional , ψ es una instancia de sustitución de φ si y sólo si ψ puede obtenerse de φ sustituyendo fórmulas por variables proposicionales en φ , reemplazando cada aparición de la misma variable por una aparición de la misma fórmula. . Por ejemplo:

(R → S) y (T → S)

es una instancia de sustitución de:

P y Q

y

(Un ↔ Un) ↔ (Un ↔ Un)

es una instancia de sustitución de:

(Un ↔ Un)

En algunos sistemas de deducción para lógica proposicional, se puede ingresar una nueva expresión (una proposición ) en una línea de una derivación si es una instancia de sustitución de una línea anterior de la derivación (Hunter 1971, p. 118). Así se introducen nuevas líneas en algunos sistemas axiomáticos . En sistemas que utilizan reglas de transformación , una regla puede incluir el uso de una instancia de sustitución con el fin de introducir ciertas variables en una derivación.

Tautologías

Una fórmula proposicional es una tautología si es verdadera bajo cada valoración (o interpretación ) de sus símbolos predicados. Si Φ es una tautología y Θ es una instancia de sustitución de Φ, entonces Θ es nuevamente una tautología. Este hecho implica la solidez de la regla de deducción descrita en el apartado anterior.

Lógica de primer orden

En lógica de primer orden , una sustitución es una aplicación total σ : VT de variables a términos ; muchos, [1] : 73  [2] : 445  pero no todos [3] : 250  autores requieren adicionalmente σ ( x ) = x para todas las variables x , excepto un número finito . La notación { x 1  ↦  t 1 , …, x k  ↦  t k } [nota 1] se refiere a una sustitución que asigna cada variable x i al término correspondiente t i , para i =1,…, k y cualquier otra variable a sí mismo; la x i debe ser distinta por pares. La aplicación de esa sustitución a un término t se escribe en notación sufija como t { x 1  ↦  t 1 , ..., x k  ↦  t k }; significa reemplazar (simultáneamente) cada aparición de cada x i en t por ti . [nota 2] El resultado de aplicar una sustitución σ a un término t se llama instancia de ese término t . Por ejemplo, aplicando la sustitución { x  ↦  z , z  ↦  h ( a , y ) } al término

El dominio dom ( σ ) de una sustitución σ se define comúnmente como el conjunto de variables realmente reemplazadas, es decir, dom ( σ ) = { xV | x }. Una sustitución se denomina sustitución fundamental si asigna todas las variables de su dominio a términos fundamentales , es decir, libres de variables. La instancia de sustitución de una sustitución fundamental es un término fundamental si todas las variables de t están en el dominio de σ, es decir, si vars ( t ) dom ( σ ) . Una sustitución σ se llama sustitución lineal si es un término lineal para algún (y por tanto cada) término lineal t que contiene precisamente las variables del dominio de σ , es decir, con vars ( t ) = dom ( σ ). Una sustitución σ se llama sustitución plana si es una variable para cada variable x . Una sustitución σ se denomina sustitución de cambio de nombre si es una permutación en el conjunto de todas las variables. Como toda permutación, una sustitución de cambio de nombre σ siempre tiene una sustitución inversa σ −1 , tal que tσσ −1 = t = −1 σ para cada término t . Sin embargo, no es posible definir una inversa para una sustitución arbitraria.

Por ejemplo, { x  ↦ 2, y  ↦ 3+4 } es una sustitución terrestre, { x  ↦  x 1 , y  ↦  y 2 +4 } no es terrestre ni plana, pero es lineal, { x  ↦  y 2 , y  ↦  y 2 +4 } es no lineal y no plano, { x  ↦  y 2 , y  ↦  y 2 } es plano, pero no lineal, { x  ↦  x 1 , y  ↦  y 2 } es lineal y plano, pero no es un cambio de nombre, ya que asigna tanto y como y 2 a y 2 ; cada una de estas sustituciones tiene el conjunto { x , y } como dominio. Un ejemplo de sustitución de nombre es { x  ↦  x 1 , x 1  ↦  y , y  ↦  y 2 , y 2  ↦  x }, tiene la inversa { x  ↦  y 2 , y 2  ↦  y , y  ↦  x 1 , x 1  ↦  x }. La sustitución plana { x  ↦  z , y  ↦  z } no puede tener una inversa, ya que, por ejemplo, ( x + y ) { x  ↦  z , y  ↦  z } = z + z , y el último término no se puede transformar nuevamente en x + y , ya que se pierde la información sobre el origen del que proviene az . La sustitución fundamental { x  ↦ 2 } no puede tener una inversa debido a una pérdida similar de información de origen, por ejemplo, en ( x +2) { x  ↦ 2 } = 2+2, incluso si algún tipo de método ficticio permitiera reemplazar constantes por variables. "sustituciones generalizadas".

Dos sustituciones se consideran iguales si asignan cada variable a términos de resultado sintácticamente iguales , formalmente: σ = τ si = para cada variable xV . La composición de dos sustituciones σ = { x 1  ↦  t 1 , …, x k  ↦  t k } y τ = { y 1  ↦  u 1 , …, y l  ↦ u l } se obtiene eliminando de la sustitución { x 1  ↦  t 1 τ , …, x k  ↦  t k τ , y 1  ↦  u 1 , …, y l  ↦  u l } aquellos pares y i  ↦  u i para los cuales y i ∈ { x 1 , …, x k }. La composición de σ y τ se denota por στ . La composición es una operación asociativa y es compatible con la aplicación de sustitución, es decir ( ρσ ) τ = ρ ( στ ) y ( ) τ = t ( στ ), respectivamente, para cada sustitución ρ , σ , τ y cada término t. . La sustitución de identidad , que asigna cada variable a sí misma, es el elemento neutral de la composición de sustitución. Una sustitución σ se llama idempotente si σσ = σ y, por tanto, tσσ = para cada término t . Cuando x it i para todo i , la sustitución { x 1  ↦  t 1 , …, x k  ↦  t k } es idempotente si y solo si ninguna de las variablesx i ocurre en cualquier t j . La composición de sustitución no es conmutativa, es decir, στ puede ser diferente de τσ , incluso si σ y τ son idempotentes. [1] : 73–74  [2] : 445–446 

Por ejemplo, { x  ↦ 2, y  ↦ 3+4 } es igual a { y  ↦ 3+4, x  ↦ 2 }, pero diferente de { x  ↦ 2, y  ↦ 7 }. La sustitución { x  ↦  y + y } es idempotente, por ejemplo (( x + y ) { xy + y }) { xy + y } = (( y + y )+ y ) { xy + y } = ( y + y )+ y , mientras que la sustitución { x  ↦  x + y } no es idempotente, por ejemplo (( x + y ) { xx + y }) { xx + y } = (( x + y )+ y ) { xx + y } = (( x + y )+ y )+ y . Un ejemplo de sustituciones sin conmutación es { x  ↦  y } { y  ↦  z } = { x  ↦  z , y  ↦  z }, pero { y  ↦  z } { x  ↦  y } = { x  ↦  y , y  ↦  z } .

Álgebra

La sustitución es una operación básica en álgebra , en particular en álgebra informática . [4] [5]

Un caso común de sustitución involucra polinomios , donde la sustitución de un valor numérico (u otra expresión) por el indeterminado de un polinomio univariado equivale a evaluar el polinomio en ese valor. De hecho, esta operación ocurre con tanta frecuencia que la notación de polinomios a menudo se adapta a ella; en lugar de designar un polinomio con un nombre como P , como se haría con otros objetos matemáticos, se podría definir

de modo que la sustitución de X pueda designarse reemplazando dentro de " P ( X )", digamos

o

La sustitución también se puede aplicar a otros tipos de objetos formales construidos a partir de símbolos, por ejemplo, elementos de grupos libres . Para que se defina la sustitución, se necesita una estructura algebraica con una propiedad universal apropiada , que afirme la existencia de homomorfismos únicos que envían indeterminados a valores específicos; la sustitución equivale entonces a encontrar la imagen de un elemento bajo tal homomorfismo.

La sustitución está relacionada con la composición de funciones , pero no es idéntica a ella ; está estrechamente relacionado con la reducción β en el cálculo lambda . Sin embargo, en contraste con estas nociones, el énfasis en álgebra está en la preservación de la estructura algebraica mediante la operación de sustitución, el hecho de que la sustitución da un homomorfismo para la estructura en cuestión (en el caso de polinomios, la estructura de anillo ). [ cita necesaria ]

Ver también

Notas

  1. ^ Algunos autores utilizan [ t 1 / x 1 ,…, t k / x k ] para denotar esa sustitución, por ejemplo, M. Wirsing (1990). Jan van Leeuwen (ed.). Especificación algebraica . Manual de informática teórica. vol. B. Elsevier. págs. 675–788., aquí: pág. 682.
  2. ^ Desde el punto de vista del álgebra de términos , el conjunto T de términos es el álgebra de términos libre sobre el conjunto V de variables, por lo tanto, para cada mapeo de sustitución σ: VT hay un homomorfismo único σ : TT que concuerda con σ en VT ; La aplicación de σ definida anteriormente a un término t se considera entonces como la aplicación de la función σ al argumento t .

Citas

  1. ^ ab David A. Duffy (1991). Principios de la demostración automatizada de teoremas . Wiley.
  2. ^ ab Franz Baader , Wayne Snyder (2001). Alan Robinson y Andrei Voronkov (ed.). Teoría de la unificación (PDF) . Elsevier. págs. 439–526. Archivado desde el original (PDF) el 8 de junio de 2015 . Consultado el 24 de septiembre de 2014 .
  3. ^ N. Dershowitz; J.-P. Jouannaud (1990). "Reescribir sistemas". En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. vol. B. Elsevier. págs. 243–320.
  4. ^ Margret H. Hoft; Hartmut FW Hoft (6 de noviembre de 2002). Computación con Mathematica. Elsevier. ISBN 978-0-08-048855-4.
  5. ^ Andre Heck (6 de diciembre de 2012). Introducción al arce . Medios de ciencia y negocios de Springer. ISBN 978-1-4684-0484-5. sustitución.

Referencias

enlaces externos