En ciencias de la computación , Programming Computable Functions (PCF) es un lenguaje funcional mecanografiado introducido por Gordon Plotkin en 1977, basado en material previo inédito de Dana Scott . [nota 1] Puede considerarse una versión extendida del cálculo lambda tipado o una versión simplificada de lenguajes funcionales tipados modernos como ML o Haskell .
A completamente abstracto modelo para PCF fue dado primero por Milner (1977). Sin embargo, dado que el modelo de Milner se basó esencialmente en la sintaxis de PCF, se consideró menos que satisfactorio (Ong, 1995). Los dos primeros modelos completamente abstractos que no empleaban sintaxis se formularon durante la década de 1990. Estos modelos se basan en la semántica de los juegos (Hyland y Ong, 2000; Abramsky, Jagadeesan y Malacaria, 2000) y las relaciones lógicas de Kripke (O'Hearn y Riecke, 1995). Durante un tiempo se consideró que ninguno de estos modelos era completamente satisfactorio, ya que no eran efectivamente presentables. Sin embargo, Ralph Loader demostró que no podría existir un modelo completamente abstracto presentable de manera efectiva, ya que la cuestión de la equivalencia del programa en el fragmento final de PCF no es decidible.
Sintaxis
Los tipos de PCF se definen inductivamente como
- nat es un tipo
- Para los tipos σ y τ , existe un tipo σ → τ
Un contexto es una lista de pares x: σ , donde x es un nombre de variable y σ es un tipo, de modo que no se duplica ningún nombre de variable. A continuación, se definen los juicios mecanográficos de términos en contexto de la forma habitual para las siguientes construcciones sintácticas:
- Variables (si x: σ es parte de un contexto Γ , entonces Γ ⊢ x : σ )
- Aplicación (de un término de tipo σ → τ a un término de tipo σ )
- λ-abstracción
- El combinador de punto fijo Y (formando términos de tipo σ a partir de términos de tipo σ → σ )
- Las operaciones sucesor ( succ ) y predecesor ( pred ) en nat y la constante 0
- El condicional if con la regla de escritura:
- ( nat s se interpretará como booleanos aquí con una convención como cero que denota verdad y cualquier otro número que denote falsedad)
Semántica
Semántica denotacional
Una semántica relativamente sencilla para el lenguaje es el modelo de Scott . En este modelo,
- Los tipos se interpretan como ciertos dominios .
- Un contexto se interpreta como el producto
- Términos en contexto se interpretan como funciones continuas
- Los términos variables se interpretan como proyecciones
- La abstracción y aplicación de Lambda se interpretan haciendo uso de la estructura cerrada cartesiana de la categoría de dominios y funciones continuas.
- Y se interpreta tomando el punto menos fijo del argumento
Este modelo no es completamente abstracto para PCF; pero es completamente abstracto para el lenguaje obtenido al agregar un operador paralelo u a PCF (p. 293 en la referencia de Hyland y Ong 2000 a continuación).
Notas
- ^ "PCF es un lenguaje de programación para funciones computables, basado en LCF, la lógica de funciones computables de Scott" ( Plotkin 1977 ). La programación de funciones computables es utilizada por ( Mitchell 1996 ). También se conoce como Programación con funciones computables o Lenguaje de programación para funciones computables .
Referencias
- Scott, Dana S. (1969). "Una alternativa teórica de tipos a CUCH, ISWIM, OWHY" (PDF) . Manuscrito inédito . Apareció como Scott, Dana S. (1993). "Una alternativa teórica de tipos a CUCH, ISWIM, OWHY". Informática Teórica . 121 : 411–440. doi : 10.1016 / 0304-3975 (93) 90095-b .
- Plotkin, Gordon D. (1977). "LCF considerado como lenguaje de programación" (PDF) . Informática Teórica . 5 (3): 223-255. doi : 10.1016 / 0304-3975 (77) 90044-5 .
- Milner, Robin (1977). "Modelos totalmente abstractos de λ-cálculos" (PDF) . Informática Teórica . 4 : 1–22. doi : 10.1016 / 0304-3975 (77) 90053-6 .
- Mitchell, John C. (1996). "El lenguaje PCF". Fundamentos de los lenguajes de programación .
- Abramsky, S., Jagadeesan, R. y Malacaria, P. (2000). "Abstracción completa para PCF" . Información y Computación . 163 (2): 409–470. doi : 10.1006 / inco.2000.2930 .CS1 maint: varios nombres: lista de autores ( enlace )
- Hyland, JME y Ong, C.-HL (2000). "Sobre la abstracción completa para PCF" . Información y Computación . 163 (2): 285–408. doi : 10.1006 / inco.2000.2917 .
- O'Hearn, PW y Riecke, J. G (1995). "Relaciones lógicas de Kripke y PCF" . Información y Computación . 120 (1): 107-116. doi : 10.1006 / inco.1995.1103 .
- Cargador, R. (2001). "Finitary PCF no es decidible". Informática Teórica . 266 (1–2): 341–364. doi : 10.1016 / S0304-3975 (00) 00194-8 .
- Ong, C.-HL (1995). "Correspondencia entre semántica operacional y denotacional: el problema de abstracción total para PCF" . En Abramsky, S .; Gabbay, D .; Maibau, TSE (eds.). Manual de Lógica en Informática . Prensa de la Universidad de Oxford. págs. 269–356. Archivado desde el original el 7 de enero de 2006 . Consultado el 19 de enero de 2006 .
enlaces externos
- Introducción a RealPCF
- Lexer y analizador para PCF escritos en SML