Comparación de enfoques para administrar variables libres y vinculadas.

Question

Comparación de enfoques para administrar variables libres y vinculadas.

greg nisbet

Correcciones:

originalmente dije $\varphi(x, w_1 \cdots w_n, a)$ era una fórmula bien formada cerrada. No lo es. Quise decir que dentro $\varphi$ las únicas variables libres provienen de $x, w_1 \cdots w_n, a$ , es decir $\text{FV}(\varphi) \subset \{x, w_1 \cdots w_n, a\}$ .

Comparación de enfoques para administrar variables libres y vinculadas.

¿Cuáles son los diferentes enfoques para administrar variables libres y vinculadas en fórmulas bien formadas? ¿Hay alguna referencia que compare explícitamente múltiples formas de hacerlo y hable sobre sus ventajas y desventajas?

Por ejemplo, aquí está el esquema de especificación del axioma de Z(F)(C) tal como lo presenta Wikipedia, pero con todas las variables en minúsculas y algunos cambios de notación menores.

\forall w_{1} \dots w_{norte} . \forall a . \exists b . \forall X . (X \in b) \leftrightarrow (X \in a \land φ (X_{1}, w_{1} \dots w_{norte}, a))

$\forall w_1\cdots w_n \mathop. \forall a \mathop. \exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in a \land \varphi(x_1, w_1 \cdots w_n, a))$

Tenga en cuenta que todos los símbolos de variables están vinculados.

En la convención utilizada en el artículo, $\varphi$ es una fórmula bien formada. $\varphi(x_1, w_1 \cdots w_n, a)$ es una fórmula bien formada y el hecho de que $b$ no aparece en $(x_1, w_1 \cdots w_n, a)$ es significante. El hecho de que $b$ no ocurre significa que $b$ no ocurre libre en $\varphi$ . No estoy seguro de cómo definir $\varphi(\vec{v})$ por un arbitrario $\vec{v}$ en esta notación... suelo pensar en ello como una forma de declarar dependencias en algún sentido donde la interpretación exacta depende del contexto.

Creo que hay algunas ventajas técnicas al definir la sintaxis para hacer que los símbolos de variables enlazadas y libres sean disjuntos. No inventé la idea de separar variables libres y enlazadas, pero no recuerdo dónde lo vi.

Sea una letra latina minúscula un símbolo de variable ligada y una letra latina mayúscula un símbolo de variable libre. Dejar $\psi[M:=\chi]$ ser una sustitución que evita la captura reemplazando $M$ con $\chi$ en la fórmula bien formada $\psi$ .

Usando esta convención, la fórmula anterior se puede escribir de la siguiente manera.

\exists b . \forall X . (X \in b) \leftrightarrow (X \in A \land φ [X := X])

$\exists b \mathop. \forall x \mathop. (x \in b) \leftrightarrow (x \in A \land \varphi[X:=x])$

En este caso, $\varphi$ es una fórmula ordinaria bien formada sin restricciones. $A$ podría ocurrir en $\varphi$ o puede que no. $X$ podría ocurrir en $\varphi$ o puede que no. En virtud de estar bien formado $b$ no puede ocurrir libre en $\varphi$ ya que es inherentemente una variable ligada. Sin embargo, es un poco extraño que los nombres de las variables libres en $\varphi$ no son irrelevantes; $X$ y $A$ ambos tienen significados especiales debido a la redacción exacta del esquema del axioma.

Entonces, en este caso particular, usar una colección distinta de símbolos para variables libres y ligadas parece simplificar parte de mi tarea al definir un esquema de axioma, pero puede que no sea más conveniente en general.

thorimur

¡Puede que encuentres los índices de Bruijn relevantes! puede haber literatura que compare los índices de Bruijn con otros métodos de vinculación, lo que podría proporcionar un punto de partida.

Alex Kruckmann

¿Estás seguro de que quieres decir eso?

φ

$\varphi$ es una fórmula cerrada ? "Fórmula cerrada" generalmente significa lo mismo que "oración": sin variables libres. Pero

x, w_{1}, \dots, w_{n}, a

$x,w_1,\dots,w_n,a$ todo puede ocurrir libre en

φ

$\varphi$ .

greg nisbet

Quise decir que los argumentos para

φ

$\varphi$ capturar todas las dependencias que

φ

$\varphi$ tiene (y por lo tanto la ausencia de

b

$b$ es significativo). Cerrado definitivamente no es la palabra correcta, pero no sé qué es.

Alex Kruckmann

la notación

φ (v_{1}, \dots, v_{n})

$\varphi(v_1,\dots,v_n)$ se suele utilizar para indicar las variables libres de la fórmula

φ

$\varphi$ se encuentran entre

v_{1}, \dots, v_{n}

$v_1,\dots,v_n$ . Es decir, cada variable libre en

φ

$\varphi$ es uno de

v_{i}

$v_i$ , pero no todos los

v_{i}

$v_i$ necesidad de ocurrir libre en

φ

$\varphi$ . Esta es una notación muy útil, porque podemos escribir

φ (a_{1}, \dots, a_{n})

$\varphi(a_1,\dots,a_n)$ para la operación de sustitución

a_{i}

$a_i$ por cada instancia libre de

v_{i}

$v_i$ . Y deja claro que

φ

$\varphi$ define naturalmente un subconjunto de

A^{n}

$A^n$ / un

n

$n$ relación -aria en

A

$A$ , para cualquier estructura

A

$A$ .

Alex Kruckmann

Por lo general, no es necesario indicar de manera similar las variables vinculadas en una fórmula

φ

$\varphi$ , porque una vez vinculados, sus identidades son irrelevantes. Es decir, puede intercambiar una variable vinculada (en su cuantificador y en cada instancia dentro del alcance de ese cuantificador) por una variable diferente sin cambiar el significado de la fórmula.

greg nisbet

Gracias. Lo que siempre encontré confuso sobre

φ (\vec{v})

$\varphi(\vec{v})$ es que se usaba tanto para decir

FV (φ) \subset \vec{v}

$\text{FV}(\varphi) \subset \vec{v}$ y decir

φ [x_{1} := {\vec{v}}_{1} \dots x_{n} := {\vec{v}}_{n}]

$\varphi[x_1 := \vec{v}_1 \cdots x_n := \vec{v}_n]$ dónde

x_{i}

$x_i$ es el

i

$i$ th variable libre ... así que siempre me pregunté si el "nombre" del parámetro o su posición en la lista de argumentos era más importante. // Los índices de De Bruijn son otra buena alternativa. Los he visto antes en discusiones sobre cálculo lambda, aunque la sustitución no es trivial y requiere que agregues.

Mauro ALLEGRANZA

Existe el enfoque utilizado por Gentzen (el padre de ND y Sequent Calc) para separar variables:

x, y

$x,y$ usado solo enlazado, de parámetros :

a, b

$a,b$ usado solo gratis. Ejemplo con

\forall

$\forall$ -Regla de introducción:

\frac{φ}{\forall x φ [x / a]}

$\dfrac {\varphi} {\forall x \varphi [x/a]}$

Marcas.

Creo que algunas lecturas relacionadas (pero no exhaustivas) podrían estar esparcidas en la documentación de Metamath Proof Explorer, por ejemplo, ZFC Axioms Without Distinct Variable Conditions .

Respuestas (1)

Comparación de enfoques para administrar variables libres y vinculadas.

¡Puede que encuentres los índices de Bruijn relevantes! puede haber literatura que compare los índices de Bruijn con otros métodos de vinculación, lo que podría proporcionar un punto de partida.
¿Estás seguro de que quieres decir eso? $\varphi$ es una fórmula cerrada ? "Fórmula cerrada" generalmente significa lo mismo que "oración": sin variables libres. Pero $x,w_1,\dots,w_n,a$ todo puede ocurrir libre en $\varphi$ .
Quise decir que los argumentos para $\varphi$ capturar todas las dependencias que $\varphi$ tiene (y por lo tanto la ausencia de $b$ es significativo). Cerrado definitivamente no es la palabra correcta, pero no sé qué es.
la notación $\varphi(v_1,\dots,v_n)$ se suele utilizar para indicar las variables libres de la fórmula $\varphi$ se encuentran entre $v_1,\dots,v_n$ . Es decir, cada variable libre en $\varphi$ es uno de $v_i$ , pero no todos los $v_i$ necesidad de ocurrir libre en $\varphi$ . Esta es una notación muy útil, porque podemos escribir $\varphi(a_1,\dots,a_n)$ para la operación de sustitución $a_i$ por cada instancia libre de $v_i$ . Y deja claro que $\varphi$ define naturalmente un subconjunto de $A^n$ / un $n$ relación -aria en $A$ , para cualquier estructura $A$ .
Por lo general, no es necesario indicar de manera similar las variables vinculadas en una fórmula $\varphi$ , porque una vez vinculados, sus identidades son irrelevantes. Es decir, puede intercambiar una variable vinculada (en su cuantificador y en cada instancia dentro del alcance de ese cuantificador) por una variable diferente sin cambiar el significado de la fórmula.
Gracias. Lo que siempre encontré confuso sobre $\varphi(\vec{v})$ es que se usaba tanto para decir $\text{FV}(\varphi) \subset \vec{v}$ y decir $\varphi[x_1 := \vec{v}_1 \cdots x_n := \vec{v}_n]$ dónde $x_i$ es el $i$ th variable libre ... así que siempre me pregunté si el "nombre" del parámetro o su posición en la lista de argumentos era más importante. // Los índices de De Bruijn son otra buena alternativa. Los he visto antes en discusiones sobre cálculo lambda, aunque la sustitución no es trivial y requiere que agregues.
Existe el enfoque utilizado por Gentzen (el padre de ND y Sequent Calc) para separar variables: $x,y$ usado solo enlazado, de parámetros : $a,b$ usado solo gratis. Ejemplo con $\forall$ -Regla de introducción: $\dfrac {\varphi} {\forall x \varphi [x/a]}$
Creo que algunas lecturas relacionadas (pero no exhaustivas) podrían estar esparcidas en la documentación de Metamath Proof Explorer, por ejemplo, ZFC Axioms Without Distinct Variable Conditions .

Pedro Smith · Answer 1

"Creo que hay algunas ventajas técnicas al definir la sintaxis para hacer que los símbolos de variables enlazadas y libres se separen. No inventé la idea de separar las variables libres y enlazadas, pero no recuerdo dónde lo vi". El dispositivo de usar diferentes letras para variables vinculadas [es decir, variables que sirven para vincular prefijos cuantificadores a lugares en predicados simples o complejos] y para variables libres [expresiones cuyo uso principal es como parámetros/nombres ficticios/nombres "arbitrarios", como usted prefiera para decirlo] está presente en las investigaciones de deducción natural originales de Gentzen de la década de 1930, y luego nuevamente en el libro clásico de Prawitz de 1965. Se recoge en algunos libros de texto de lógica influyentes posteriores, comenzando con los de Lemmon y Thomason.

Dependiendo exactamente de cómo configure las cosas, el dispositivo, entre otras cosas, le permite evitar preocuparse por la captura involuntaria de variables. Pero quizás la principal razón positiva para adoptar el dispositivo no sea técnica sino [en un sentido amplio] filosófica o conceptual: se adhiere al muy buen principio fregeano de marcar claramente en la sintaxis importantes diferencias de rol semántico .

Comparación de enfoques para administrar variables libres y vinculadas.

greg nisbet

thorimur

Alex Kruckmann

greg nisbet

Alex Kruckmann

Alex Kruckmann

greg nisbet

Mauro ALLEGRANZA

Marcas.

Respuestas (1)

Pedro Smith

¿Artículos sobre ideas en la historia de la notación matemática?

¿La suma de dos expresiones lineales es siempre una expresión lineal?

¿Se puede introducir formalmente la notación de creación de conjuntos en ZFC?

¿Es la teoría de los lenguajes formales regulares finitamente axiomatizable?

¿Es correcta esta notación de intervalo para la solución de un problema de desigualdad?

Un proyecto de trabajo sobre topología algebraica (con sabor categórico): sugerencias de temas.

Teorema que inspiró a Dennis Sullivan a cambiarse a las matemáticas

¿Texto de geometría de la escuela secundaria?

¿Cómo traduzco 'ningún estudiante de filosofía admira a ningún profesor podrido' en una fórmula lógica cuantificacional?

Definición de rango de términos en lenguaje de primer orden