Hay una receta de dos pasos para esto:
1. Defina lo que significa que ocurra un error de tipo.
2. Probar que no puede suceder.
- ¿Qué industrias serán las últimas en utilizar el aprendizaje automático?
- ¿Podemos usar el viaje en el tiempo para resolver problemas de NP?
- ¿Cómo encuentro una pasantía en una empresa tecnológica francesa?
- ¿Qué módulos funcionales de SAP son más relevantes / más cercanos a la informática?
- ¿Cómo describirías a los miembros de la facultad en el departamento de CS de tu universidad?
Un error común es descuidar la importancia del paso 1.
El resto de la respuesta es desde la perspectiva de probar la seguridad de tipos para los idiomas escritos. Las personas que hablan informalmente sobre idiomas no tipificados usan el término “tipo seguro” para significar algo diferente pero relacionado, y probar la seguridad de los tipos generalmente no es una preocupación.
Por lo general, hacemos el paso 1 dando una semántica para el lenguaje en el que algunas transiciones no están definidas. Por ejemplo, puede dar una semántica en la que el programa true + "bees" simplemente no tiene un resultado. La forma preferida de hacer esto hoy (a menos que tenga que lidiar con algo extraño) es dar una semántica de reducción , que es una semántica que modela la ejecución de un programa mediante una secuencia de pasos, cada uno de los cuales produce un nuevo programa. Por ejemplo, aquí hay una secuencia de reducción para una expresión aritmética:
[matemáticas] 3 \ veces5 + 8 \ veces (4-3) [/ matemáticas]
[matemáticas] \ mapsto15 + 8 \ veces (4-3) [/ matemáticas]
[matemáticas] \ mapsto15 + 8 \ times1 [/ matemáticas]
[matemáticas] \ mapsto15 + 8 [/ matemáticas]
[matemáticas] \ mapsto23 [/ matemáticas]
Es posible extender esto a lenguajes mucho más ricos que tienen funciones, E / S, control, etc. No siempre es obvio cómo, por lo que hay algo de arte involucrado.
Usualmente hacemos el paso 2 en términos de solidez de tipo, que es la propiedad de que el sistema de tipo no miente. (He incluido una versión de lo siguiente en la parte inferior para aquellos de ustedes que prefieren conjuntos y relaciones). Un sistema de tipos generalmente hace declaraciones como “expresión [matemáticas] e [/ matemáticas] tiene tipo [matemáticas] \ tau [ / math] “, que entendemos que significa que evaluar [math] e [/ math] nos dará una respuesta de tipo [math] \ tau [/ math]. El teorema de solidez de tipo genérico se ve así:
Teorema (Tipo de solidez). Si el término (programa) [matemática] e [/ matemática] tiene el tipo [matemática] \ tau [/ matemática], entonces la evaluación (ejecución) [matemática] e [/ matemática] diverge (se ejecuta para siempre) o termina con una respuesta [ math] v [/ math] que también tiene el tipo [math] \ tau [/ math].
Una forma común de probar esto es dividiéndolo en dos lemas:
Lema (Progreso). Si un programa está bien escrito, entonces ha terminado con una respuesta o puede tomar un paso de evaluación.
Lemma (Preservación). Si un programa tiene algún tipo y da un paso, el programa resultante tiene el mismo tipo.
El teorema sigue trivialmente.
Esta técnica es de Andrew Wright y Matthias Felleisen “A Syntactic Approach to Type Soundness”. Hay muchas otras formas de hacerlo, pero en su mayoría son más difíciles, por lo que no las usaría a menos que fuera necesario.
Aquí está la versión para matemáticos.
Definición. Un lenguaje de programación escrito es un quíntuple [matemático] (P, A, \ mathit {pasos}, T, \ mathit {typeof}) [/ math], donde:
– [math] P [/ math] es un conjunto de programas ;
– [matemáticas] A \ subseteq {P} [/ matemáticas] es un conjunto de respuestas distinguidas;
– [math] \ mathit {steps} \ subseteq {(P \ backslash {A})} \ times {P} [/ math] relaciona los programas que no responden con los programas;
– [math] T [/ math] es un conjunto de tipos ; y
– [math] \ mathit {typeof} \ subseteq {P} \ times {T} [/ math] relaciona los programas con los tipos.
Deje que [math] \ mathit {steps} ^ * [/ math] denote el cierre reflexivo y transitivo de [math] \ mathit {steps} [/ math].
Definición. Un programa [math] p \ in {P} [/ math] diverge si para todos [math] p ‘\ in {P} [/ math] tal que [math] \ mathit {pasos} ^ * (p, p’ ) [/ math], existe algo de [math] p ” \ en {P} [/ math] tal que [math] \ mathit {steps} (p ‘, p’ ‘) [/ math].
Definición (Tipo de solidez). Un lenguaje de programación mecanografiado [matemáticas] (P, A, \ mathit {pasos}, T, \ mathit {typeof}) [/ math] goza de solidez de tipo si para todos los programas [math] p \ in {P} [/ math] y escribe [math] \ tau \ en {T} [/ math] tal que [math] \ mathit {typeof} (p, \ tau) [/ math], [math] p [/ math] diverge o existe algunos responden [math] a \ en {A} [/ math] de modo que [math] \ mathit {steps} ^ * (p, a) [/ math], y para todos esos [math] a [/ math], [math] \ mathit {typeof} (a, \ tau) [/ math].
Por lo general, probamos la solidez del tipo mediante dos lemas estándar:
Lema (Progreso). Para todos [math] p \ in {P} [/ math] y [math] \ tau \ in {T} [/ math] tal que [math] \ mathit {typeof} (p, \ tau) [/ math] , [math] p \ in {A} [/ math] o existe alguna [math] p ‘\ in {P} [/ math] tal que [math] \ mathit {steps} (p, p’) [ /mates].
Lemma (Preservación). Para todos [math] p, p ‘\ in {P} [/ math] y [math] \ tau \ in {T} [/ math], if [math] \ mathit {typeof} (p, \ tau) [ / math] y [math] \ mathit {pasos} (p, p ‘) [/ math], luego [math] \ mathit {typeof} (p’, \ tau) [/ math].
Hay algunos detalles que pueden diferir aquí dependiendo de si [math] \ mathit {steps} [/ math] y [math] \ mathit {typeof} [/ math] son funciones parciales o relaciones arbitrarias, pero esa es la idea general. Además, esa definición de lenguaje de programación mecanografiado está lejos de ser la única forma de hacerlo, pero probablemente sea la más común entre los investigadores de lenguaje de programación en la actualidad.
