Una lógica no estándar admisible para programas funcionales

  1. Gil Luezas, Ana
Zuzendaria:
  1. María Teresa Hortala González Zuzendaria

Defentsa unibertsitatea: Universidad Complutense de Madrid

Defentsa urtea: 1990

Epaimahaia:
  1. José F. Prida Presidentea
  2. Juan Carlos Martínez Alonso Idazkaria
  3. José Luis Balcázar Navarro Kidea
  4. María Gracia Manzano Arjona Kidea
  5. Fernando Orejas Valdés Kidea

Mota: Tesia

Teseo: 25038 DIALNET lock_openDocta Complutense editor

Laburpena

SON PRESENTADOS ALGUNOS LENGUAJES FORMALES PARA EL ESTUDIO DE LOS PROGRAMAS FUNCIONALES, EL LENGUAJE MAS AMPLIAMENTE TRATADO ES EL LRF, ESTE LENGUAJE CONSTA DE EXPRESIONES FUNCIONALES, QUE REPRESENTAN A LOS PROGRAMAS FUNCIONALES, Y DE FORMULAS, LAS CUALES PERMITEN RAZONAR SOBRE EL COMPORTAMIENTO DE LOS PROGRAMAS. SE DEMUESTRA QUE VARIAS LOGICAS DE PROGRAMAS YA CONOCIDAS, COMO EL CALCULO PROPORCIONAL DE KOZEN Y LA LOGICA DE PRIMER ORDEN DINAMICA, SON EXPRESABLES EN LRF. SE DEMUESTRA TAMBIEN QUE LRF ES UN FRAGMENTO DEL LENGUAJE INFINITARIO LWUW. FINALMENTE, SE OBTIENEN TEOREMAS DE CORRECCION Y COMPLEJITUD PARA ESTE LENGUAJE. EN LA SEGUNDA PARTE DEL TRABAJO SE INTRODUCE UN LENGUAJE NO ESTANDARD ADMISIBLE PARA PROGRAMAS FUNCIONALES, AL QUE SE LE LLAMA ALRF. SE DEMUESTRA QUE ESTE LENGUAJE ADMITE UN CALCULO CORRECTO Y COMPLETO, Y ORIENTADO A LA SINTAXIS, TOMANDO COMO REFERENCIA A LA CLASE DE LOS MODELOS ADMISIBLES. SE MUESTRA ADEMAS QUE ES POSIBLE EXPRESAR EN ALRF LA TERMINACION DE PROGRAMAS NO TRIUJALES, CONTRARIAMENTE A LO QUE SUCEDE CON EL LENGUAJE LRF.