lambda-calculus

13El calor

1Respuesta

Ejemplo de teorema de iglesia-rosser en un lenguaje de programación funcional

He visto referencias múltiples al Church Rosser theorem, y en particular al diagrama de propiedad de diamante, mientras aprendo programación funcional pero no he encontrado un gran ejemplo de código.

11El calor

1Respuesta

¿Cómo encontrar la orden de procesamiento óptima?

Tengo una pregunta interesante, pero no estoy seguro exactamente cómo expresarlo ... Considere el cálculo lambda. Para una expresión dada de lambda, hay varias órdenes de reducción posibles. Pero algu

9El calor

1Respuesta

¿Cómo usar un contexto de nomenclatura para encontrar índices de Bruijn de variables libres?

En "Tipos y lenguajes de programación", en la sección 6.1.2 se habla de un contexto de nomenclatura utilizado para numerar variables libres en expresiones lambda. Usando el esquema de ejemplo que han

9El calor

1Respuesta

¿Cuáles son algunos tipos y/o términos en el sistema-f que no se pueden expresar en Hindley Milner

Recuerdo haber leído en alguna parte que Hindley Milner era una restricción en el sistema-f. Si ese es el caso, ¿podría alguien proporcionarme algunos términos que pueden escribirse en el sistema-f pe

5El calor

3Respuesta

El tipo de firma de un combinador no coincide con la firma de tipo de su función Lambda equivalente

consideran este combinador: S (S K) aplicarlo a los argumentos XY: S (S K) X Y Se contrae a: X Y Convertí S (SK) a los términos Lambda correspondientes y obtuve este resultado: (\x y -> x y) h

7El calor

3Respuesta

Incrustar tipos de mayor kínder (¡mónadas!) En el cálculo lambda sin tipo

Es posible codificar varios tipos en el cálculo lambda sin tipo a través de funciones de orden superior. Examples: zero = λfx. x one = λfx. fx two = λfx. f(fx) three = λfx. f(f(fx)) etc true

5El calor

1Respuesta

¿Los parámetros implícitos son una dificultad para incluir en GHC?

Tengo curiosidad sobre las objeciones a implicit parameters discutidas en el artículo Functional Pearl: Implicit Configurations por Kiselyov y Shan. No es correcto el código en línea (β-reduce) en pre

5El calor

1Respuesta

Lo que hace esto combinador hacer: s (SK)

Ahora entiendo la firma tipo de s (s k): s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 Y puede crear ejemplos que funcionan sin error en la herramienta de Haskell WinGHCi: Ejemplo: s (s k) (\g -

26El calor

3Respuesta

listas Iglesia en Haskell

que tenían que implementar la función de mapa de Haskell para trabajar con las listas de la iglesia que se definen de la siguiente manera: type Churchlist t u = (t->u->u)->u->u En el cálculo lambda,

24El calor

3Respuesta

¿Qué se entiende por "sustituciones que evitan la captura"?

Al leer el cálculo de Lambda en Wiki, se encontró con el término sustituciones que evitan la captura. ¿Puede alguien explicar por qué significa que no pude encontrar una definición desde ningún lugar?