Cómo formalizar un operador de enlace de variables, como $\frac{d}{dx}$ ?

Question

Cómo formalizar un operador de enlace de variables, como $\frac{d}{dx}f(x)$ ? Por ejemplo, creo que deberíamos tratar $\frac{d}{dx}$ como una función de orden superior de $x$ , devolviendo una función que toma como argumento (normalmente una expresión de su letra sea mencionada, digamos $x$ Por ejemplo $x^2+1$ ) a su expresión correspondiente (por ejemplo $2x$ ). Algunos ejemplos son:

1. $(\frac{d}{dx})(3x^2+4x)=6x+4$

2. $(\frac{d}{dz})(3z^2+4z)=6z+4$

3. $(D_y)\cos y=-\sin y$ ( $D_y$ equivale a $\frac{d}{dy}$ )

Los matemáticos, o lógicos, suelen decir que $\frac{d}{dx}$ es una de las llamadas variable-vinculante lo que significa que la letra (es decir, la variable) especificada en el $d(\cdot)$ es sólo una variable independiente, que está ligada al símbolo, y no se ve afectada por las variables de soporte externas. Así que se puede escribir una expresión como definir $f(x)=\frac{d}{dx}(x^2)$ y obtener $f(10)=(2x)|_{x=10}=20$ no $f(10)=\frac{d}{d10}(10^2)$ . Esto último no tiene sentido.

De manera normal, los estudiantes de grado aprenden sobre un definición de la función no existe tal forma de hacer un mecanismo de vinculación de variables en la definición de la función simple (a través de relación n-aria ). ¡No hay lugar para que digamos (especifiquemos) en la definición de una función que ésta debe mantener sus argumentos sin evaluar e independientes!

El otro operador relacionado es $\sum$ como por ejemplo $\displaystyle\sum_{i=1}^{10}i^2$ También tiene la función (no es un juego de palabras) de vincular variables.

Entonces, mi pregunta es: ¿cómo formalizar estas cosas? ¿Es posible? ¿Ya lo han discutido los lógicos? ¿Existe una forma estándar que sea aceptada por la gente?

Answer 1

La comunidad informática cuenta con una vasta literatura sobre este tema, ya que cuando se implementan sistemas no se tiene la opción de ser permisivo con lo que se quiere decir exactamente con una forma vinculante. Por ejemplo, existe un blog dedicado precisamente a esto que menciona muchos enfoques diferentes.

Lo más sencillo, desde el punto de vista matemático, es tratar estas operaciones como funciones de orden superior, es decir, funciones que toman funciones (a menudo llamadas "funcionales" en matemáticas.) Esto no resuelve realmente el problema, sino que lo traslada a un caso (no tan) "bien entendido". Por ejemplo, se trataría la diferenciación unidimensional como una función $D : \mathbb{R}^\mathbb{R}\to\mathbb{R}^\mathbb{R}$ y así la diferenciación de $x + ax^2$ sería $D(x \mapsto x + ax^2)$ . Una cosa buena de esta perspectiva es que te hace pensar un poco más en lo que está pasando. Por ejemplo, debes considerar cuál sería un tipo preciso para la diferenciación de varias variables o la integración de una sola variable.

Aun así, en la práctica este enfoque puede resultar bastante opaco o requerir funciones "anónimas", como el ejemplo que he utilizado anteriormente, que, como he dicho, es donde se desplaza el problema. Podrías evitar las funciones anónimas en este caso definiendo versiones elevadas de la suma y la multiplicación y constantes y definiendo $x$ como la función de identidad. Entonces se podría escribir $D(x+ax^2)$ . No se puede reemplazar $x$ con $y$ , en este caso, como $y$ simplemente no está definida (aunque también se podría definir como la función de identidad). Si se tratara del caso de múltiples variables, se podría definir $x$ como la primera proyección de una 2-tupla, y $y$ como la segunda proyección, y conseguir una sintaxis de aspecto "normal", pero probablemente causaría mucha confusión si se intentara seguir rigurosamente este enfoque. Probablemente sería más claro en ese punto, utilizar explícitamente la identidad y la proyección como valores, es decir $D(\mathsf{id}+a\mathsf{id}^2)$ o $D(\pi_1 + \pi_2)$ para $\nabla(x+y)$ .

Si quiere detallar los pormenores de la manipulación de la unión de nombres, la mayoría de las introducciones a la cálculo lambda que básicamente no es más que funciones anónimas, dará una descripción básica de cómo se maneja. En particular, las nociones de equivalencia alfa y de sustitución que evita la captura. La plétora de enfoques que mencioné al principio está impulsada, en informática, por preocupaciones como la facilidad de implementación, la facilidad de probar resultados, la eficiencia de la implementación y las construcciones de enlace "no estándar" como las que estarían presentes en, por ejemplo, el cálculo lambda lineal .