Factorización de derivaciones a través de tipos intersección
En sistemas de tipos intersección no idempotentes típicos, la normalización de pruebas no es confluente. En este trabajo presentamos un sistema confluente de tipos intersección no idempotentes para el cálculo λ. Escribimos las derivaciones de tipos usando una sintaxis concisa de términos de prueba....
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Tesis de Grado |
| Lenguaje: | Español |
| Publicado: |
28 d
|
| Materias: | |
| Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000445_CiruelosRodriguez |
| Aporte de: |
| Sumario: | En sistemas de tipos intersección no idempotentes típicos, la normalización de pruebas no es confluente. En este trabajo presentamos un sistema confluente de tipos intersección no idempotentes para el cálculo λ. Escribimos las derivaciones de tipos usando una sintaxis concisa de términos de prueba. El sistema goza de buenas propiedades: subject reduction, es fuertemente normalizante, y tiene una teoría de residuos muy regular. Establecemos una correspondencia con el cálculo lambda mediante teoremas de simulación. La maquinaria de los tipos intersección no idempotentes nos permite seguir el rastro del uso de los recursos necesarios para obtener una respuesta. En particular, induce una noción de basura: un cómputo es basura si no contribuye a hallar una respuesta. Usando estas nociones, mostramos que el espacio de derivaciones de un término λ puede ser factorizado usando una variante de la construcción de Grothendieck para semireticulados. Esto significa, en particular, que cualquier derivación del cálculo λ puede ser escrita de una única manera como un prefijo libre de basura, seguido de basura. |
|---|