Un enfoque para tales preguntas es a través de codificaciones .
Digamos que tiene un idioma L1 y un idioma L2 y desea mostrar que de alguna manera son "iguales", puede hacer esto buscando una codificación
[[⋅]]:L1→L2
y luego demuestre que para todos los programas cumple lo siguiente:L1M,N
M≅1Niff[[M1]]≅2[[M2]]
Aquí es una noción elegida de equivalencia de programa para . Con el fin de hacer esto para lenguajes de tipos, uno mapas normalmente también -Tipos a por medio de una función que se extiende a entornos de escritura, tales que algo así se cumple lo siguiente:L i L 1 L 2 ⌜ ⋅≅iLiL1L2┌⋅┐
⊢ i
Γ⊢1M:αimplies┌Γ┐⊢2[[M]]:┌α┐
Aquí es el juicio de tipeo para . Todo el enfoque se llama
abstracción completa .
⊢iLi
Con el fin de evitar la "maldición de la universalidad de la Iglesia-Turing", uno típicamente impone condiciones en , por ejemplo, que es compositivo, o cerrado bajo cambio de nombre inyectivo. más condiciones , más fuerte será el resultado de la abstracción completa.[[[⋅]][[⋅]]
Esto también es lo que intentan hacer Orchard y Yoshida (Teoremas 1 a 5), aunque no lo logran.