Codificación Mogensen-Scott

Forma de representar los tipos de datos en el cálculo lambda

En informática , la codificación Scott es una forma de representar tipos de datos (recursivos) en el cálculo lambda . La codificación Church realiza una función similar. Los datos y los operadores forman una estructura matemática que está incorporada en el cálculo lambda.

Mientras que la codificación de Church comienza con representaciones de los tipos de datos básicos y avanza a partir de ellos, la codificación de Scott comienza con el método más simple para componer tipos de datos algebraicos .

La codificación Mogensen–Scott extiende y modifica levemente la codificación Scott al aplicar la codificación a la metaprogramación ^{[ cita requerida ]} . Esta codificación permite la representación de términos de cálculo lambda , como datos, para ser utilizados por un metaprograma.

Historia

La codificación Scott aparece por primera vez en un conjunto de notas de clase inéditas de Dana Scott ^[1], cuya primera cita aparece en el libro Combinatorial Logic, Volume II . ^[2] Michel Parigot dio una interpretación lógica y un recurso fuertemente normalizador para los numerales codificados por Scott, ^[3] refiriéndose a ellos como la representación de números de "tipo pila". Torben Mogensen luego extendió la codificación Scott para la codificación de términos Lambda como datos. ^[4]

Discusión

El cálculo lambda permite almacenar datos como parámetros de una función que aún no tiene todos los parámetros necesarios para su aplicación. Por ejemplo,

${\displaystyle ((\lambda x_{1}\ldots x_{n}.\lambda c.c\ x_{1}\ldots x_{n})\ v_{1}\ldots v_{n})\ f}$

Puede considerarse como un registro o estructura donde los campos se han inicializado con los valores . A continuación, se puede acceder a estos valores aplicando el término a una función f . Esto se reduce a, ${\displaystyle x_{1}\ldots x_{n}}$ ${\displaystyle v_{1}\ldots v_{n}}$

${\displaystyle f\ v_{1}\ldots v_{n}}$

c puede representar un constructor para un tipo de datos algebraicos en lenguajes funcionales como Haskell . Ahora supongamos que hay N constructores, cada uno con argumentos; ${\displaystyle A_{i}}$

${\displaystyle {\begin{array}{c|c|c}{\text{Constructor}}&{\text{Given arguments}}&{\text{Result}}\\\hline ((\lambda x_{1}\ldots x_{A_{1}}.\lambda c_{1}\ldots c_{N}.c_{1}\ x_{1}\ldots x_{A_{1}})\ v_{1}\ldots v_{A_{1}})&f_{1}\ldots f_{N}&f_{1}\ v_{1}\ldots v_{A_{1}}\\((\lambda x_{1}\ldots x_{A_{2}}.\lambda c_{1}\ldots c_{N}.c_{2}\ x_{1}\ldots x_{A_{2}})\ v_{1}\ldots v_{A_{2}})&f_{1}\ldots f_{N}&f_{2}\ v_{1}\ldots v_{A_{2}}\\\vdots &\vdots &\vdots \\((\lambda x_{1}\ldots x_{A_{N}}.\lambda c_{1}\ldots c_{N}.c_{N}\ x_{1}\ldots x_{A_{N}})\ v_{1}\ldots v_{A_{N}})&f_{1}\ldots f_{N}&f_{N}\ v_{1}\ldots v_{A_{N}}\end{array}}}$

Cada constructor selecciona una función diferente de los parámetros de la función . Esto proporciona ramificaciones en el flujo del proceso, en función del constructor. Cada constructor puede tener una aridad (número de parámetros) diferente. Si los constructores no tienen parámetros, el conjunto de constructores actúa como una enumeración ; un tipo con un número fijo de valores. Si los constructores tienen parámetros, se pueden construir estructuras de datos recursivas. ${\displaystyle f_{1}\ldots f_{N}}$

Definición

Sea D un tipo de datos con N constructores , , tales que el constructor tiene aridad . ${\displaystyle \{c_{i}\}_{i=1}^{N}}$ ${\displaystyle c_{i}}$ ${\displaystyle A_{i}}$

Codificación Scott

La codificación Scott del constructor del tipo de datos D es ${\displaystyle c_{i}}$

${\displaystyle \lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}\ x_{1}\ldots x_{A_{i}}}$

Codificación Mogensen-Scott

Mogensen extiende la codificación Scott para codificar cualquier término lambda sin tipo como datos. Esto permite que un término lambda se represente como datos dentro de un metaprograma de cálculo lambda . La función meta mse convierte un término lambda en la representación de datos correspondiente del término lambda;

${\displaystyle {\begin{aligned}\operatorname {mse} [x]&=\lambda a,b,c.a\ x\\\operatorname {mse} [M\ N]&=\lambda a,b,c.b\ \operatorname {mse} [M]\ \operatorname {mse} [N]\\\operatorname {mse} [\lambda x.M]&=\lambda a,b,c.c\ (\lambda x.\operatorname {mse} [M])\\\end{aligned}}}$

El "término lambda" se representa como una unión etiquetada con tres casos:

• Constructor a - una variable ( aridad 1, no recursiva)
• Constructor b - aplicación de la función (aridad 2, recursiva en ambos argumentos),
• Constructor c - abstracción lambda (aridad 1, recursivo).

Por ejemplo,

${\displaystyle {\begin{array}{l}\operatorname {mse} [\lambda x.f\ (x\ x)]\\\lambda a,b,c.c\ (\lambda x.\operatorname {mse} [f\ (x\ x)])\\\lambda a,b,c.c\ (\lambda x.\lambda a,b,c.b\ \operatorname {mse} [f]\ \operatorname {mse} [x\ x])\\\lambda a,b,c.c\ (\lambda x.\lambda a,b,c.b\ (\lambda a,b,c.a\ f)\ \operatorname {mse} [x\ x])\\\lambda a,b,c.c\ (\lambda x.\lambda a,b,c.b\ (\lambda a,b,c.a\ f)\ (\lambda a,b,c.b\ \operatorname {mse} [x]\ \operatorname {mse} [x]))\\\lambda a,b,c.c\ (\lambda x.\lambda a,b,c.b\ (\lambda a,b,c.a\ f)\ (\lambda a,b,c.b\ (\lambda a,b,c.a\ x)\ (\lambda a,b,c.a\ x)))\end{array}}}$

Comparación con la codificación de la Iglesia

La codificación Scott coincide con la codificación Church para valores booleanos. La codificación Church de pares se puede generalizar a tipos de datos arbitrarios mediante la codificación de D anterior como ^{[ cita requerida ]} ${\displaystyle c_{i}}$

${\displaystyle \lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}(x_{1}c_{1}\ldots c_{N})\ldots (x_{A_{i}}c_{1}\ldots c_{N})}$

compare esto con la codificación Mogensen Scott,

${\displaystyle \lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}x_{1}\ldots x_{A_{i}}}$

Con esta generalización, las codificaciones de Scott y Church coinciden en todos los tipos de datos enumerados (como el tipo de datos booleano) porque cada constructor es una constante (sin parámetros).

En cuanto a la viabilidad de utilizar la codificación Church o Scott para la programación, existe una compensación simétrica: ^[5] los numerales codificados por Church admiten una operación de suma en tiempo constante y no son mejores que una operación predecesora en tiempo lineal; los numerales codificados por Scott admiten una operación predecesora en tiempo constante y no son mejores que una operación de suma en tiempo lineal.

Definiciones de tipos

Los datos codificados por Church y las operaciones con ellos se pueden tipificar en el sistema F , al igual que los datos y las operaciones codificados por Scott. Sin embargo, la codificación es significativamente más complicada. ^[6]

El tipo de codificación Scott de los números naturales es el tipo recursivo positivo:

${\displaystyle \mu X.\forall R.R\to (X\to R)\to R}$

Los tipos recursivos completos no son parte del Sistema F, pero los tipos recursivos positivos se pueden expresar en el Sistema F a través de la codificación:

${\displaystyle \mu X.G[X]=\forall X.((G[X]\to X)\to X)}$

Combinando estos dos hechos se obtiene el tipo Sistema F de la codificación Scott:

${\displaystyle \forall X.(((\forall R.R\to (X\to R)\to R)\to X)\to X)}$

Esto puede contrastarse con el tipo de codificación de la Iglesia:

${\displaystyle \forall X.X\to (X\to X)\to X}$

¡La codificación de la Iglesia es un tipo de segundo orden, pero la codificación de Scott es de cuarto orden!

Véase también

• Codificación de la iglesia
• Sistema F
• Cubo lambda

Notas

1. Scott, Dana (1968) [1962]. Un sistema de abstracción funcional . Conferencias dictadas en la Universidad de California, Berkeley.
2. Curry, Haskell (1972). Lógica combinatoria, volumen II . North-Holland Publishing Company. ISBN 0-7204-2208-6.
3. Parigot, Michel (1988). "Programación con pruebas: una teoría de tipos de segundo orden". En H. Ganzinger (ed.). Simposio Europeo de Programación: ESOP '88 . 2º Simposio Europeo de Programación. Nancy, Francia, 21-24 de marzo de 1988. Lecture Notes in Computer Science. Vol. 300. Springer. pp. 145-159. doi : 10.1007/3-540-19027-9_10 . ISBN 978-3-540-19027-1.
4. Mogensen, Torben (1994). "Autointerpretación eficiente en cálculo lambda". Revista de programación funcional . 2 (3): 345–364. doi :10.1017/S0956796800000423. S2CID  8736707.
5. Parigot, Michel (1990). "Sobre la representación de datos en el cálculo lambda". En Egon Börger; Hans Kleine Büning; Michael M. Richter (eds.). Taller internacional sobre lógica informática: CSL '89 . Tercer taller sobre lógica informática. Kaiserslautern, RFA, 2-6 de octubre de 1989. Lecture Notes in Computer Science. Vol. 440. Springer. pp. 209–321. doi :10.1007/3-540-52753-2_47. ISBN 978-3-540-52753-4.
6. Véase la nota "Tipos para los numerales Scott" de Martín Abadi, Luca Cardelli y Gordon Plotkin (18 de febrero de 1993).

Referencias

• Stump, A. (2009). Metaprogramación directamente reflexiva. Higher-Order and Symbolic Computation, 22 , 115-144.
• Mogensen, T.Æ. (1992). Autointerpretaciones eficientes en cálculo lambda. J. Funct. Program., 2 , 345-363.