Sustitución

En matemáticas e informática , la sustitución es la operación de reemplazo sintáctico de subtérminos de un término dado por otros términos, según ciertas reglas. Por lo general, estamos hablando de sustituir un término en lugar de una variable .

Definiciones y notación

No existe una notación universal y coherente para la sustitución, ni existe una definición estándar. El concepto de sustitución varía no solo dentro de las secciones, sino también a nivel de publicaciones individuales. En general, podemos distinguir la sustitución de contexto y la sustitución "en lugar de" . En el primer caso, el lugar del término donde se produce la sustitución viene dado por el contexto , es decir, la parte del término que “rodea” ese lugar. En particular, tal noción de sustitución se utiliza en la reescritura . La segunda opción es más común. En este caso, la sustitución suele estar dada por alguna función del conjunto de variables al conjunto de términos. Para denotar la acción de sustitución , por regla general, utilice la notación de sufijo . Por ejemplo, significa el resultado de una acción de sustitución en un término . ${\ estilo de visualización \ sigma: X \ a T}$ ${\ estilo de visualización t \ sigma}$ $\sigma$ $t$

En la gran mayoría de los casos se requiere que la sustitución tenga un soporte finito, es decir, que el conjunto sea finito. En este caso, se puede especificar mediante una simple enumeración de pares de valores de variables . Dado que cada una de estas sustituciones se puede reducir a una secuencia de sustituciones que reemplazan solo una variable cada una, sin pérdida de generalidad, podemos suponer que la sustitución está dada por un par variable-valor , lo que generalmente se hace. ${\displaystyle \{x\mid x\neq \sigma x\))$

La última definición de sustitución es probablemente la más típica y la más utilizada. Sin embargo, tampoco existe una notación única generalmente aceptada para ello. La notación más común para sustituir a por x en t es t [ a / x ], t [ x := a ] o t [ x ← a ].

Sustitución de variables en cálculo λ

En el cálculo de λ, la sustitución se define por inducción estructural. Para objetos arbitrarios y una variable arbitraria, el resultado de reemplazar una ocurrencia libre arbitraria en se considera una sustitución y se determina por inducción de construcción : $PAGS$ $q$ $X$ $X$ $q$ $q$

(i) base: : el objeto es lo mismo que la variable . Entonces ;

Q\equiv x

q

X

[P/x]x\equiv P

(ii) base: : el objeto es lo mismo que la constante . Entonces para atómico arbitrario ;

Q\equiv c

q

C

{\ estilo de visualización [P/x] c \ equivalente c}

c\no \equiv x

(iii) paso: : el objeto no es atómico y tiene la forma de una aplicación . Entonces ;

Q\equiv (Q_{1}\,Q_{2})

q

{\ estilo de visualización (Q_{1}\,Q_{2})}

[P/x](Q_{1}\,Q_{2})\equiv ([P/x]Q_{1})([P/x]Q_{2})

(iv) paso: : el objeto no es atómico y es una abstracción de . Entonces [ ;

Q\equiv\lambda xM

q

X

{\ estilo de visualización \ lambda xM}

P/x](\lambda xM)\equiv \lambda xM

(v) paso: : el objeto no es atómico y es una abstracción de , con . Después:

Q\equiv\lambda yM

q

y

\lambda yM

y\no \equiv x

[P/x](\lambda yM)\equiv (\lambda y.[P/x]M)

para y o ;

y\no \equiv x

y\notin P

x\notin M

{\ estilo de visualización (\ lambda z. [P/x] [z/y] M)}

para y y .

y\no \equiv x

{\ estilo de visualización y \ en P}

x \en M

Véase también

Enlaces

Lógicas

Filosofía • Semántica • Sintaxis • Historia

Grupos lógicos

lógica clásica	lógica aristotélica Lógica proposicional Lógica de primer orden Lógica de segundo orden lógica de orden superior
lógica matemática	teoría de conjuntos Teoría del modelo teoría de la computabilidad Teoría de la prueba y matemáticas constructivas lógica lineal sistema formal conclusión natural cálculo de secuencias Álgebra de la lógica Lógica relevante lógica deóntica lógica intuicionista cálculo de Lambek
Lógica no clásica	intuicionismo lógica difusa Lógica subestructural lógica Descripción lógica Lógica multivaluada Síntesis lógica Lógica vinculante Lógica temporal Lógica modal ( Lógica híbrida ) lógica epistémica
lógica filosófica	Pensamiento crítico lógica informal razonamiento deductivo

Componentes

Lista de símbolos booleanos