Variable fresca

En el razonamiento formal, en particular en la lógica matemática , el álgebra computacional y la demostración automática de teoremas , una variable nueva es una variable que no se presentaba en el contexto considerado hasta el momento. ^{[1] [ cita requerida ]} El concepto se utiliza a menudo sin explicación. ^{[2] [ cita requerida ]}

Las variables nuevas se pueden utilizar para reemplazar otras variables, para eliminar el sombreado o captura de variables. Por ejemplo, en la conversión alfa , el procesamiento de términos en el cálculo lambda en términos equivalentes con variables renombradas, reemplazar variables con variables nuevas puede ser útil como una forma de evitar capturar accidentalmente variables que deberían estar libres . ^[3] Otro uso para las variables nuevas implica el desarrollo de invariantes de bucle en la verificación formal de programas , donde a veces es útil reemplazar constantes por variables nuevas recién introducidas. ^[4]

Ejemplo

Por ejemplo, en la reescritura de términos , antes de aplicar una regla a un término dado , cada variable en debe reemplazarse por una nueva para evitar conflictos con las variables que ocurren en . ^{[ cita requerida ]} Dada la regla ${\displaystyle l\to r}$ ${\displaystyle t}$ ${\displaystyle l\to r}$ ${\displaystyle t}$

${\displaystyle append(cons(x,y),z)\to cons(x,append(y,z))}$

y el término

${\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))}$,

Intentar encontrar una sustitución coincidente del lado izquierdo de la regla, , dentro de fallará, ya que no puede coincidir con . Sin embargo, si la regla se reemplaza por una copia nueva ^[a] ${\displaystyle append(cons(x,y),z)}$ ${\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))}$ ${\displaystyle y}$ ${\displaystyle cons(y,nil)}$

${\displaystyle append(cons(v_{1},v_{2}),v_{3})\to cons(v_{1},append(v_{2},v_{3}))}$

Antes, la coincidencia tendrá éxito con la sustitución de la respuesta . ${\displaystyle \{v_{2}\mapsto x,\;v_{2}\mapsto cons(y,nil),\;v_{3}\mapsto cons(3,nil)\}}$

Notas

1. es decir, una copia con cada variable reemplazada consistentemente por una variable nueva

Referencias

1. Carmen Bruni (2018). Lógica de predicados: deducción natural (PDF) (Diapositivas de la conferencia). Univ. de Waterloo.Aquí: diapositiva 13/26.
2. Michael Färber (febrero de 2023). Semántica denotacional y un intérprete rápido para jq (informe técnico). Univ. de Innsbruck. arXiv : 2302.10576 .Aquí: p.4.
3. Gordon, Andrew D.; Melham, Thomas F. (1996). "Cinco axiomas de conversión alfa". En von Wright, Joakim; Grundy, Jim; Harrison, John (eds.). Demostración de teoremas en lógicas de orden superior, 9.ª conferencia internacional, TPHOLs'96, Turku, Finlandia, 26-30 de agosto de 1996, Actas . Apuntes de clase en informática. Vol. 1125. Springer. págs. 173-190. doi :10.1007/BFB0105404.
4. Cohen, Edward (1990). "Loops B — On replacement constants by fresh variables" (Bucles B: sobre la sustitución de constantes por nuevas variables). Programación en la década de 1990. Monografías en Ciencias de la Computación. Nueva York: Springer. pp. 149–194. doi :10.1007/978-1-4613-9706-9. ISBN 9781461397069.S2CID 1509875  .