Programación de funciones computables

En ciencias de la computación , Programación de Funciones Computables (PCF), o Programación con Funciones Computables, o Lenguaje de Programación para Funciones Computables, es un lenguaje de programación tipado y basado en la programación funcional , introducido por Gordon Plotkin en 1977 , ^[¹^] basado en material previo no publicado de Dana Scott . ^[^a^] Puede considerarse como 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 propuso por primera vez un modelo totalmente abstracto para PCF . ^[²^] Sin embargo, dado que el modelo de Milner se basaba esencialmente en la sintaxis de PCF, se consideró poco satisfactorio. ^[³^] Los dos primeros modelos totalmente abstractos que no empleaban sintaxis se formularon durante la década de 1990. Estos modelos se basan en la semántica de juegos ^[⁴^]^[⁵^] y las relaciones lógicas de Kripke. ^[⁶^] 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 podía existir un modelo totalmente abstracto efectivamente presentable, puesto que la cuestión de la equivalencia de programas en el fragmento finito de PCF no es decidible. ^[⁷^]

Sintaxis

Los tipos de datos de PCF se definen inductivamente como

nat es un tipo
Para los tipos σ y τ , existe un tipo de función σ → τ.

Un contexto es una lista de pares x : σ , donde x es un nombre de variable y σ es un tipo, de manera que ningún nombre de variable se duplique. A continuación, se definen los juicios de tipado de los 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 crea términos de tipo σ a partir de términos de tipo σ → σ )
Las operaciones de sucesor ( succ ) y predecesor ( pred ) sobre nat y la constante 0
La condición if con la regla de tipado:

{\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 valores `nat` se interpretarán como booleanos, siguiendo una convención en la que cero denota verdad y cualquier otro número denota 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 .
- $[\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }$ (los números naturales con un elemento inferior adjunto, con el orden plano)
- $[\![\sigma \to \tau \,]\!]$ se interpreta como el dominio de funciones continuas de Scott desde $[\![\sigma ]\!]\,$ a $[\![\tau ]\!]\,$ , con el ordenamiento punto por punto.
Un contexto $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ se interpreta como el producto $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$
Términos en contexto $\Gamma \;\vdash \;x\;:\;\sigma$ $\Gamma \;\vdash \;x\;:\;\sigma$ se interpretan como funciones continuas $[\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]$ $[\![\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 fijo más pequeño del argumento.

Este modelo no es completamente abstracto para PCF; pero sí lo es para el lenguaje obtenido al agregar un operador paralelo o "or" a PCF. ^{[ 4 ]}^{: 293}

Notas

↑ "PCF es un lenguaje de programación para funciones computables, basado en LCF, la lógica de funciones computables de Scott."^{[ 1 ]} Programación de funciones computables es utilizado por ( Mitchell 1996 ).

Referencias

1 2 Plotkin, Gordon D. (diciembre de 1977). "LCF considerado como un lenguaje de programación" (PDF) . Theoretical Computer Science . 5 (3): 223– 255. doi : 10.1016/0304-3975(77)90044-5 .
↑ Milner, Robin (febrero de 1977). "Modelos totalmente abstractos de λ-cálculos tipados" (PDF) . Theoretical Computer Science . 4 (1): 1– 22. doi : 10.1016/0304-3975(77)90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
↑ Ong, C.-HL (1995). "Correspondencia entre la semántica operacional y denotacional: el problema de la abstracción completa para PCF" . En Abramsky, S.; Gabbay, D.; Maibau, TSE (eds.). Manual de lógica en informática . Oxford University Press. pp. 269–356 . Archivado del original el 7 de enero de 2006. Recuperado el 19 de enero de 2006 .
1 2 Hyland, JME; Ong, C.-HL (15 de diciembre de 2000). "Sobre la abstracción completa para PCF" . Información y computación . 163 (2): 285– 408. doi : 10.1006/inco.2000.2917 .
↑ Abramsky, S.; Jagadeesan, R.; Malacaria, P. (15 de diciembre de 2000). "Abstracción completa para PCF" . Information and Computation . 163 (2): 409– 470. doi : 10.1006/inco.2000.2930 .
↑ O'Hearn, PW; Riecke, JG (1995). "Relaciones lógicas de Kripke y PCF" . Información y computación . 120 (1): 107– 116. doi : 10.1006/inco.1995.1103 .
↑ Loader, R. (2001). "El PCF finito no es decidible" . Theoretical Computer Science . 266 ( 1–2 ): 341–364 . doi : 10.1016/S0304-3975(00)00194-8 .

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 de los lenguajes de programación . MIT Press. ISBN 9780262133210.

Enlaces externos

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

[2] "PCF es un lenguaje de programación para funciones computables, basado en LCF, la lógica de funciones computables de Scott."^{[ 1 ]} Programación de funciones computables es utilizado por ( Mitchell 1996 ).

[Plotkin_1977-1] 1 2 Plotkin, Gordon D. (diciembre de 1977). "LCF considerado como un lenguaje de programación" (PDF) . Theoretical Computer Science . 5 (3): 223– 255. doi : 10.1016/0304-3975(77)90044-5 .

[Milner_1977-3] Milner, Robin (febrero de 1977). "Modelos totalmente abstractos de λ-cálculos tipados" (PDF) . Theoretical Computer Science . 4 (1): 1– 22. doi : 10.1016/0304-3975(77)90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .

[Ong_1995-4] Ong, C.-HL (1995). "Correspondencia entre la semántica operacional y denotacional: el problema de la abstracción completa para PCF" . En Abramsky, S.; Gabbay, D.; Maibau, TSE (eds.). Manual de lógica en informática . Oxford University Press. pp. 269–356 . Archivado del original el 7 de enero de 2006. Recuperado el 19 de enero de 2006 .

[Hyland_2000-5] 1 2 Hyland, JME; Ong, C.-HL (15 de diciembre de 2000). "Sobre la abstracción completa para PCF" . Información y computación . 163 (2): 285– 408. doi : 10.1006/inco.2000.2917 .

[Abramsky_2000-6] Abramsky, S.; Jagadeesan, R.; Malacaria, P. (15 de diciembre de 2000). "Abstracción completa para PCF" . Information and Computation . 163 (2): 409– 470. doi : 10.1006/inco.2000.2930 .

[O'Hearn_1995-7] O'Hearn, PW; Riecke, JG (1995). "Relaciones lógicas de Kripke y PCF" . Información y computación . 120 (1): 107– 116. doi : 10.1006/inco.1995.1103 .

[Loader_2001-8] Loader, R. (2001). "El PCF finito no es decidible" . Theoretical Computer Science . 266 ( 1–2 ): 341–364 . doi : 10.1016/S0304-3975(00)00194-8 .

[

[

[

[

[

[

[

[