Programación de funciones computables

En informática , Programming Computable Functions (PCF) es un lenguaje funcional tipado introducido por Gordon Plotkin en 1977, ^[1] basado en material previo no publicado 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 .

Robin Milner fue el primero en proponer un modelo completamente abstracto para PCF . ^[2] Sin embargo, dado que el modelo de Milner se basaba esencialmente en la sintaxis de PCF, se consideró poco satisfactorio. ^[3] 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 juegos ^{[4] [5]} y en las relaciones lógicas de Kripke. ^[6] Durante un tiempo se creyó que ninguno de estos modelos era completamente satisfactorio, ya que no eran efectivamente presentables. Sin embargo, Ralph Loader demostró que no podía existir un modelo completamente abstracto efectivamente presentable, ya que la cuestión de la equivalencia de programas en el fragmento finitario de PCF no es decidible. ^[7]

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 ningún nombre de variable se duplique. A continuación, se definen los juicios de tipificación 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 (que forma términos de tipo σ a partir de términos de tipo σ → σ )
• Las operaciones sucesora ( succ ) y predecesora ( pred ) sobre nat y la constante 0
• El condicional if con la regla de tipificación:

${\displaystyle {\frac {\Gamma \;\vdash \;t\;:{\textbf {nat}},\quad \quad \Gamma \;\vdash \;s_{0}\;:\sigma ,\quad \quad \Gamma \;\vdash \;s_{1}\;:\sigma }{\Gamma \;\vdash \;{\textbf {si}}(t,s_{0},s_{1})\;:\sigma }}}$

( aquí los nat se interpretarán como booleanos con una convención como cero que denota verdad y cualquier otro número que denota falsedad)

Una semántica relativamente sencilla para el lenguaje es el modelo Scott . En este modelo,

• Los tipos se interpretan como ciertos dominios .
  • ${\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }}$(los números naturales con un elemento inferior adjunto, con el orden plano)
  • ${\displaystyle [\![\sigma \to \tau \,]\!]}$se interpreta como el dominio de las funciones continuas de Scott desde hasta , con ordenamiento puntual.${\displaystyle [\![\sigma ]\!]\,}$${\displaystyle [\![\tau ]\!]\,}$
• Un contexto se interpreta como el producto${\displaystyle x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}}$${\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]}$
• Los términos en contexto se interpretan como funciones continuas.${\displaystyle \Gamma \;\vdash \;x\;:\;\sigma }$${\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}$
  • Los términos variables se interpretan como proyecciones.
  • La abstracción y aplicación de Lambda se interpretan haciendo uso de la estructura cartesiana cerrada 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 sí lo es para el lenguaje obtenido al agregar un operador paralelo o a PCF. ^{[4] : 293}

• Scott, Dana S. (1969). "Una alternativa de teoría de tipos a CUCH, ISWIM, OWHY" (PDF) . Manuscrito inédito .Apareció como Scott, Dana S. (1993). "Una alternativa de teoría de tipos a CUCH, ISWIM, OWHY". Theoretical Computer Science . 121 : 411–440. doi : 10.1016/0304-3975(93)90095-b .
• Mitchell, John C. (1996). "El lenguaje PCF". Fundamentos para lenguajes de programación . ISBN 9780262133210.

• Introducción a RealPCF
• Analizador léxico y analizador sintáctico para PCF escrito en SML