Debido a la noción de Propuestas como Tipos, no hay absolutamente ninguna diferencia entre los sistemas lógicos para las pruebas matemáticas (usando la teoría del tipo dependiente) y la lógica de la informática. De hecho, después de que se propuso el Univalence Axiom, esto también se extiende a la topología y ha fusionado casi todas las matemáticas.
Cabe señalar que, al principio, la informática era una rama de las matemáticas de todos modos, rigurosa por Haskell Curry y Alan Turing. Ambos contribuyeron a la informática / lógica / matemáticas de maneras que no se pueden describir en un simple párrafo.
Ahora, avancemos un poco más por ese camino y hablemos de teoría versus realidad por un segundo. Las declaraciones que hice son ciertas para una máquina Turing, o para un programa Haskell, pero tienden a desviarse un poco más cuando ingresamos a lenguajes como C ++ o Java. Hay varias razones para esto, pero vamos al fondo.
- ¿Hay alguna buena idea sobre cómo optimizar la biblioteca matemática fundamental del sistema?
- ¿Cómo probarías que el problema máximo de conjunto independiente en los gráficos está en la clase NP?
- Para los montones máximos, ¿por qué el orden de build_maxheap () [math] n \ log (n), [/ math] cuando solo tiene que recorrer n / 2 elementos?
- ¿Cómo se puede encontrar el número de iteraciones requeridas para la integración usando la regla de Simpson para una precisión dada?
- ¿Las funciones del tipo x ^ 2, x ^ 3, x ^ n se consideran de naturaleza recursiva?
- Las matemáticas solo pueden modelar los efectos secundarios como un entorno completamente nuevo, siempre. En otras palabras, leer un personaje desde un teclado no se modela matemáticamente fácilmente , a menos que lo considere un nuevo objeto de teclado, cada vez que se solicitan datos. Así es como Haskell (y algunos otros lenguajes “puros” modelan IO). De lo contrario, el razonamiento sobre los efectos secundarios se vuelve difícil, y quedan muchas matemáticas sin resolver para manejar casos como C ++ y Java.
- Nulo es una abominación. Nulo no tiene un tipo bien definido. Podría modelarse como un objeto con un tipo, pero en última instancia actúa como un tipo superior (tipo universal) sin valor, y podría ser algo sin valor. Esto es confuso para el modelo y debe manejarse caso por caso.
- La herencia de implementación es un anatema para escribir el razonamiento teórico, porque no podemos exigir ningún requisito sobre los subtipos. Esto puede cambiar con la escritura dependiente, pero por el momento, es difícil hacer un razonamiento matemático cuando se trata de la herencia de implementación (sí, esto es diferente de la herencia de interfaz).
Entonces, en lo que respecta a esos tres ítems, la “informática de la vida real” tiene algunas diferencias con las matemáticas, ya que no tenemos sistemas teóricos fáciles de usar para lidiar fácilmente con esas tres situaciones en programas imperativos.
TLDR: Son lo mismo, pero con advertencias …
