¿Cuál es la diferencia entre el metalenguaje computacional de Moggi y el cálculo lambda de Moggi?

8

Esta es una confusión de referencia. A veces veo que la gente usa el término "metalenguaje computacional de Moggi" para referirse al cálculo presentado por Moggi, y a veces al "cálculo lambda computacional de Moggi". A veces usan λmetrol y a veces λC .

Siempre he asumido que ambos son lo mismo, pero al leer el resumen de una charla de Katsumata y Moegelberg, dice :

mostramos la plenitud de la traducción monádica de Moggi desde el cálculo lambda computacional \ lc con sumas al metalenguaje computacional \ lml con sumas utilizando el operador de elevación TT y cierre TT.

¿No son estos idiomas lo mismo? ¿Dónde se introducen específicamente con estos nombres? Parece que Moggi a veces habla del modelo λC para lo que él llama un metalenguaje, pero luego en otro artículo habla sobre el cálculo lambda computacional.

Alfarero
fuente

Respuestas:

1

La terminología puede ser un poco confusa, pero sí, hay dos idiomas, por ejemplo, en "Nociones de cómputos como mónadas" de Moggi (enlace gratuito aquí: https://core.ac.uk/download/pdf/21173011.pdf ).

En ese documento, los lenguajes se denominan λmetrol , el metalenguaje, y λpagsl el "lenguaje de programación". Creo que λpagsl desempeña el papel del cálculo lambda computacional, pero puedo estar equivocado. Un aspecto confuso es que ambos lenguajes tienen un constructor de tipo explícito T representa la mónada, pero se usan de manera diferente.

λmetrol es un lenguaje "puro" con una mónadaT , es decir, toda manipulación de la mónada es explícita en los tipos y el tipo de funciónτ1τ2 es el tipo de funciones puras. Observe la regla de vinculación (de la figura 3 en la página 9):

X:τmetrolmi1:Tτ1X1:τ1metrolmi2:Tτ2X:τmetrollmitTX1mi1yonortemi2:Tτ2

mi1 ymi2 se escriben explícitamente como términos deTτ1,Tτ2 para marcar que son efectivos. Cada expresión efectiva es realmente un término puro con tipo monádico. Esto es similar a cómo programamos con mónadas en Haskell donde Haskell desempeña el papel del metalenguaje y la mónada codifica los efectos, pero realmente siempre estamos manipulando términos "puros" (pongo "puro" entre comillas ya que Haskell tiene sus propios efectos de divergencia y error).

X:τmetrolmi:τ[τ][τ]

λpagslX:τpagslmi:ττττ

X:τpagslmi1:τ1X1:τ1pagslmi2:τ2X:τpagsllmitX1mi1yonortemi2:τ2

mi2X:τpagslmi:τ[τ]T[τ]

λpagslTTunaunit -> a->

Max nuevo
fuente