Sea la expresión

En informática, una expresión "let" asocia la definición de una función con un ámbito restringido .

La expresión "let" también puede definirse en matemáticas, donde asocia una condición booleana con un ámbito restringido.

La expresión "let" puede considerarse como una abstracción lambda aplicada a un valor. En matemáticas, una expresión "let" también puede considerarse como una conjunción de expresiones dentro de un cuantificador existencial que restringe el alcance de la variable.

La expresión `let` está presente en muchos lenguajes funcionales para permitir la definición local de una expresión, que luego se utiliza para definir otra. En algunos lenguajes funcionales, la expresión `let` se presenta en dos formas: `let` o `let rec`. `let rec` es una extensión de la expresión `let` simple que utiliza el combinador de punto fijo para implementar la recursión .

Historia

El lenguaje LCF de Dana Scott ^{[ 1 ]} fue una etapa en la evolución del cálculo lambda hacia los lenguajes funcionales modernos. Este lenguaje introdujo la expresión `let`, que ha aparecido en la mayoría de los lenguajes funcionales desde entonces.

Los lenguajes Scheme , ^{[ 2 ]} ML y, más recientemente, Haskell ^{[ 3 ]} han heredado expresiones let de LCF.

Los lenguajes imperativos con estado, como ALGOL y Pascal, implementan esencialmente una expresión `let` para definir un alcance restringido de las funciones en las estructuras de bloques.

Una cláusula " where " estrechamente relacionada, junto con su variante recursiva " where rec ", apareció ya en The mechanical evaluation of expressions de Peter Landin . ^[⁴^]

Descripción

Una expresión "let" define una función o valor para su uso en otra expresión. Además de ser una construcción utilizada en muchos lenguajes de programación funcional , es una construcción del lenguaje natural que se usa frecuentemente en textos matemáticos. Es una construcción sintáctica alternativa a una cláusula "where".

En ambos casos, la estructura completa es una expresión cuyo valor es 5. Al igual que en la estructura if-then-else, el tipo devuelto por la expresión no es necesariamente booleano.

Una expresión let viene en 4 formas principales,

En los lenguajes funcionales, la expresión `let` define funciones que pueden ser llamadas dentro de la expresión. El alcance del nombre de la función se limita a la estructura de la expresión `let`.

En matemáticas, la expresión `let` define una condición, que constituye una restricción sobre la expresión. La sintaxis también puede admitir la declaración de variables cuantificadas existencialmente, locales a la expresión `let`.

La terminología, la sintaxis y la semántica varían de un lenguaje a otro. En Scheme , `let` se usa para la forma simple y `let rec` para la forma recursiva. En ML, `let` marca solo el inicio de un bloque de declaraciones, mientras que `fun` marca el inicio de la definición de la función. En Haskell, `let` puede ser mutuamente recursivo , y el compilador determina qué se necesita.

Definición

Una abstracción lambda representa una función sin nombre. Esta es una fuente de inconsistencia en la definición de una abstracción lambda. Sin embargo, las abstracciones lambda pueden componerse para representar una función con nombre. De esta forma se elimina la inconsistencia. El término lambda,

(\lambda fz)\ (\lambda xy)

es equivalente a definir la función $f$ por $f\ x=y$ en la expresión $z$ , que puede escribirse como la expresión let ;

\operatorname {let} f\ x=y\operatorname {in} z

La expresión `let` se entiende como una expresión en lenguaje natural. Representa la sustitución de una variable por un valor. La regla de sustitución describe las implicaciones de la igualdad como sustitución.

Definición de "Dejemos de lado" en matemáticas.

En matemáticas, la expresión `let` se describe como la conjunción de expresiones. En lenguajes funcionales, también se utiliza para limitar el alcance. En matemáticas, el alcance se describe mediante cuantificadores. La expresión `let` es una conjunción dentro de un cuantificador existencial.

(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F

donde E y F son de tipo booleano.

La expresión let permite que la sustitución se aplique a otra expresión. Esta sustitución puede aplicarse dentro de un ámbito restringido, a una subexpresión. El uso natural de la expresión let es en la aplicación a un ámbito restringido (llamado lambda droping ). Estas reglas definen cómo se puede restringir el ámbito;

{\begin{cases}x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)\\x\in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F\\x\not \in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ F\end{cases}}

donde F no es de tipo booleano . A partir de esta definición se puede derivar la siguiente definición estándar de una expresión let, tal como se usa en un lenguaje funcional.

x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x:x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y

Para simplificar, el marcador que especifica la variable existencial, $x:$ , se omitirá de la expresión cuando quede claro por el contexto.

x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y

Derivación

Para obtener este resultado, primero supongamos que:

x\not \in \operatorname {FV} (L)

entonces

{\begin{aligned}L\ (\operatorname {let} x:x=y\operatorname {in} z)&\iff (\operatorname {let} x:x=y\operatorname {in} L\ z)\\&\iff x=y\land L\ z\end{aligned}}

Utilizando la regla de sustitución,

{\begin{aligned}&\iff x=y\land (L\ z)[x:=y]\\&\iff x=y\land (L[x:=y]\ z[x:=y])\\&\iff x=y\land L\ z[x:=y]\\&\implies L\ z[x:=y]\end{aligned}}

así que para todo L ,

L\operatorname {let} x:x=y\operatorname {in} z\implies L\ z[x:=y]

Dejar $L\ X=(X=K)$ donde K es una nueva variable. Entonces,

(\operatorname {let} x:x=y\operatorname {in} z)=K\implies z[x:=y]=K

Entonces,

\operatorname {let} x:x=y\operatorname {in} z=z[x:=y]

Pero desde la interpretación matemática de una reducción beta,

(\lambda x.z)\ y=z[x:=y]

Aquí, si y es una función de una variable x, no es la misma x que en z. Se puede aplicar el cambio de nombre alfa. Por lo tanto, debemos tener,

x\not \in \operatorname {FV} (y)

entonces,

x\not \in \operatorname {FV} (y)\implies \operatorname {let} x:x=y\operatorname {in} z=(\lambda x.z)\ y

Este resultado se representa en un lenguaje funcional de forma abreviada, donde el significado es inequívoco;

x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y

Aquí, la variable x se reconoce implícitamente como parte de la ecuación que define x, y como la variable en el cuantificador existencial.

No se permite levantar desde Boolean

Surge una contradicción si E se define por $E=\neg$ . En este caso,

x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)

se convierte,

\operatorname {let} x:G\operatorname {in} \neg F=\neg \ (\operatorname {let} x:G\operatorname {in} F)

y utilizando,

(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F

(\exists xG\land \neg F)=\neg \ (\exists xG\land F)

=(\exists x\neg G\lor \neg F)

Esto es falso si G es falso. Para evitar esta contradicción, no se permite que F sea de tipo booleano. Para F booleano, la declaración correcta de la regla de eliminación utiliza implicación en lugar de igualdad,

x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies (\operatorname {let} x:G\operatorname {in} E\ F\to E\ (\operatorname {let} x:G\operatorname {in} F))

Puede parecer extraño que se aplique una regla diferente para Boolean que para otros tipos. La razón de esto es que la regla,

(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F

Esto solo aplica cuando F es booleano. La combinación de ambas reglas crea una contradicción, por lo que cuando una regla se cumple, la otra no.

Uniendo expresiones let

Las expresiones pueden definirse con múltiples variables,

(\exists v\cdots \exists w\exists xE\land F)\iff \operatorname {let} v,\ldots ,w,x:E\operatorname {in} F

entonces se puede derivar,

x\not \in FV(E)\implies (\exists v\cdots \exists w\exists xE\land F)\iff (\exists v\cdots \exists w(E\land \exists xF))

entonces,

x\not \in FV(E)\implies (\operatorname {let} v,\ldots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\ldots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)

Leyes que relacionan el cálculo lambda y las expresiones let

La reducción Eta proporciona una regla para describir las abstracciones lambda. Esta regla, junto con las dos leyes derivadas anteriormente, define la relación entre el cálculo lambda y las expresiones let.

Sea la definición definida a partir del cálculo lambda.

Para evitar los posibles problemas asociados con la definición matemática , Dana Scott definió originalmente la expresión `let` a partir del cálculo lambda. Esto puede considerarse como la definición constructiva o ascendente de la expresión `let` , en contraste con la definición matemática axiomática o descendente.

La expresión let simple y no recursiva se definió como azúcar sintáctico para la abstracción lambda aplicada a un término. En esa definición,

(\operatorname {let} _{s}x=y\operatorname {in} z)\equiv (\lambda x.z)\ y

La definición de la expresión simple let se extendió posteriormente para permitir la recursión utilizando el combinador de punto fijo .

Combinador de punto fijo

El combinador de punto fijo puede representarse mediante la expresión,

\lambda f.\operatorname {let} x=f\ x\operatorname {in} x

Esta representación puede convertirse en un término lambda. Una abstracción lambda no admite referencia al nombre de la variable en la expresión aplicada, por lo que x debe pasarse como parámetro a x .

\lambda f.\operatorname {let} x\ x=f\ (x\ x)\operatorname {in} x\ x

Utilizando la regla de reducción de eta,

f\ x=y\equiv f=\lambda x.y

da,

\lambda f.\operatorname {let} x=\lambda x.f\ (x\ x)\operatorname {in} x\ x

Una expresión let puede expresarse como una abstracción lambda usando,

n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)

da,

\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))

Esta es posiblemente la implementación más sencilla de un combinador de punto fijo en cálculo lambda. Sin embargo, una reducción beta proporciona la forma más simétrica del combinador Y de Curry.

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))

expresión let recursiva

La expresión recursiva llamada "let rec" se define utilizando el combinador Y para expresiones recursivas de let.

(\operatorname {let\ rec} x=y\operatorname {in} z)\equiv (\lambda x.z)\ (Y\ (\lambda x.y))

Expresión let mutuamente recursiva

Este enfoque se generaliza para admitir la recursión mutua. Una expresión `let` recursiva mutua se puede componer reorganizando la expresión para eliminar cualquier condición `and`. Esto se logra reemplazando múltiples definiciones de función con una sola definición de función, que iguala una lista de variables a una lista de expresiones. Luego se utiliza una versión del combinador Y, llamado combinador de punto fijo polivariádico Y* ^{[ 5 ],} para calcular el punto fijo de todas las funciones simultáneamente. El resultado es una implementación recursiva mutua de la expresión `let` .

Valores múltiples

Una expresión `let` puede usarse para representar un valor que es miembro de un conjunto,

\operatorname {let} x\in X\operatorname {in} x

Bajo la aplicación de funciones , de una expresión let a otra,

{\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)\\&=\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y\\&=\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y\end{aligned}}

Pero se aplica una regla diferente al aplicar la expresión let a sí misma.

{\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)\\&=\operatorname {let} x\in X\operatorname {in} x\ x\end{aligned}}

No parece existir una regla sencilla para combinar valores. Se requiere una expresión general que represente una variable cuyo valor pertenezca a un conjunto de valores. Esta expresión debe basarse en la variable y el conjunto.

La aplicación de una función a esta forma debería generar otra expresión con la misma forma. De este modo, cualquier expresión sobre funciones con múltiples valores puede tratarse como si tuviera un solo valor.

No basta con que la forma represente únicamente el conjunto de valores. Cada valor debe tener una condición que determine cuándo la expresión toma dicho valor. La construcción resultante es un conjunto de pares de condiciones y valores, denominado «conjunto de valores». Véase la reducción de conjuntos de valores algebraicos .

Reglas para la conversión entre el cálculo lambda y las expresiones let.

Se proporcionarán metafunciones que describen la conversión entre expresiones lambda y let . Una metafunción es una función que recibe un programa como parámetro. El programa actúa como datos para el metaprograma. El programa y el metaprograma se encuentran en diferentes metaniveles.

Se utilizarán las siguientes convenciones para distinguir el programa del metaprograma,

Los corchetes [] se utilizarán para representar la aplicación de funciones en el metaprograma.
En el metaprograma, las variables se representarán con letras mayúsculas. En el programa, las variables se representarán con letras minúsculas.
$\equiv$ se utilizará para igualdades en el metaprograma.

Para simplificar, se aplicará la primera regla que indique coincidencias. Las reglas también presuponen que las expresiones lambda se han preprocesado de manera que cada abstracción lambda tenga un nombre único.

También se utiliza el operador de sustitución. La expresión $L[G:=S]$ Significa sustituir cada aparición de G en L por S y devolver la expresión. La definición utilizada se extiende para abarcar la sustitución de expresiones, a partir de la definición proporcionada en la página del cálculo lambda . La comparación de expresiones debe verificar la equivalencia alfa (cambio de nombre de las variables).

Conversión de expresiones lambda a expresiones let

Las siguientes reglas describen cómo convertir una expresión lambda en una expresión let , sin alterar la estructura.

$\operatorname {de-lambda} [V]\equiv V$
$\operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]$
$\operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]$
$\operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]$
$\operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]$
$V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]\equiv \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]$
$V\neq W\to \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]\equiv \operatorname {let} V,W:E\land F\operatorname {in} G$
$\operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F$

La regla 6 crea una variable única V, que sirve como nombre para la función.

Ejemplo

Por ejemplo, el combinador Y ,

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))

se convierte en,

\operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p

Conversión de expresiones `let` a expresiones lambda

Estas reglas revierten la conversión descrita anteriormente. Convierten una expresión `let` en una expresión `lambda`, sin alterar la estructura. No todas las expresiones `let` pueden convertirse utilizando estas reglas. Las reglas asumen que las expresiones ya están organizadas como si hubieran sido generadas por `de-lambda` .

$\operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]$
$\operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]$
$\operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]$
$\operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]$
$\operatorname {de-let} [V]\equiv V$
$V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]\equiv \operatorname {get-lambda} [V,E]$
$V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv (\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]$
$W\not \in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} G]\equiv \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} \operatorname {let} W:F\ \operatorname {in} G]$
$V\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ V=\operatorname {get-lambda} [V,E][V:=V\ V]\ \operatorname {in} L[V:=V\ V]]$
$W\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ W=\operatorname {get-lambda} [V,E][V:=V\ W]\ \operatorname {in} \operatorname {let} W:F[V:=V\ W]\ \operatorname {in} L[V:=V\ W]]$

En el cálculo lambda, no existe un equivalente estructural exacto para las expresiones `let` que contienen variables libres utilizadas recursivamente. En este caso, se requiere la adición de parámetros. Las reglas 8 y 10 añaden estos parámetros.

Las reglas 8 y 10 son suficientes para dos ecuaciones recursivas entre sí en la expresión `let` . Sin embargo, no funcionan para tres o más ecuaciones recursivas entre sí. El caso general requiere un nivel adicional de bucle, lo que complica un poco la metafunción. Las siguientes reglas reemplazan a las reglas 8 y 10 en la implementación del caso general. Se han mantenido las reglas 8 y 10 para que se pueda estudiar primero el caso más simple.

lambda-form - Convierte la expresión en una conjunción de expresiones, cada una de la forma variable = expresión .
1. $\operatorname {lambda-form} [G\ V=E]=\operatorname {lambda-form} [G=\lambda V.E]$
2. $\operatorname {lambda-form} [E\land F]=\operatorname {lambda-form} [E]\land \operatorname {lambda-form} [F]$
3. $\operatorname {lambda-form} [V=E]=V=E$ ...... donde V es una variable.
lift-vars : Obtiene el conjunto de variables que necesitan X como parámetro, porque la expresión tiene X como variable libre.
1. $X\in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{V\}$
2. $X\not \in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{\}$
3. $\operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [X.F]$
subvariables : Para cada variable del conjunto, sustitúyala por la variable aplicada a X en la expresión. Esto convierte a X en una variable pasada como parámetro, en lugar de ser una variable libre en el lado derecho de la ecuación.
1. $\operatorname {sub-vars} [E,\{V\}\cup S,X]=\operatorname {sub-vars} [E[V:=V\ X],S,X]$
2. $\operatorname {sub-vars} [E,\{\},X]=E$
de-let - Elevar cada condición en E de modo que X no sea una variable libre en el lado derecho de la ecuación.
1. ${\begin{aligned}L&=\operatorname {lambda-form} [E]\land S=\operatorname {lift-vars} [X,L]\to \operatorname {de-let} [\operatorname {let} V\ldots W,X:E\land F\ \operatorname {in} G]\\&\equiv \operatorname {de-let} [\operatorname {let} V\ldots W:\operatorname {sub-vars} [L,S,X]\ \operatorname {in} \operatorname {let} \operatorname {sub-vars} [\operatorname {lambda-form} [F],S,X]\ \operatorname {in} \operatorname {sub-vars} [G,S,X]]\end{aligned}}$

Ejemplos

Por ejemplo, la expresión let obtenida del combinador Y ,

\operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)\ \operatorname {in} p

se convierte en,

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))

Para un segundo ejemplo, tomemos la versión elevada del combinador Y ,

\operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p

se convierte en,

(\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)

Para un tercer ejemplo, la traducción de,

\operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x

es,

(\lambda x.x\ x)\ (\lambda x.\lambda f.f\ (x\ x\ f))

Por cuarto ejemplo, la traducción de,

\operatorname {let} x:x=f\ x\ \operatorname {in} x

es,

(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))

que es el famoso combinador y .

Personas clave

Dana Scott

Véase también

Referencias

↑ "PCF es un lenguaje de programación para funciones computables, basado en LCF, la lógica de funciones computables de Scott" ( Plotkin 1977 ) . Programación de funciones computables es utilizado por ( Mitchell 1996 ) . También se le conoce como Programación con funciones computables o Lenguaje de programación para funciones computables .
↑ "Esquema - Variables y expresiones Let" .
↑ Simon, Marlow (2010). "Informe del lenguaje Haskell 2010 - Expresiones Let" .
↑ Landin, Peter J. (1964). "La evaluación mecánica de expresiones" . The Computer Journal . 6 (4). British Computer Society : 308–320 . doi : 10.1093/comjnl/ 6.4.308 .
↑ "Combinadores de punto fijo polivariádicos más simples para recursión mutua" .

Obras citadas

Mitchell, John C. (1996). Fundamentos de los lenguajes de programación . MIT Press. ISBN 978-0-262-13321-0.
Plotkin, GD (diciembre de 1977). "LCF considerado como un lenguaje de programación" . Theoretical Computer Science . 5 (3): 223– 255. doi : 10.1016/0304-3975(77)90044-5 .

[1] "PCF es un lenguaje de programación para funciones computables, basado en LCF, la lógica de funciones computables de Scott" ( Plotkin 1977 ) . Programación de funciones computables es utilizado por ( Mitchell 1996 ) . También se le conoce como Programación con funciones computables o Lenguaje de programación para funciones computables .

[scheme-let-2] "Esquema - Variables y expresiones Let" .

[haskell-let-3] Simon, Marlow (2010). "Informe del lenguaje Haskell 2010 - Expresiones Let" .

[4] Landin, Peter J. (1964). "La evaluación mecánica de expresiones" . The Computer Journal . 6 (4). British Computer Society : 308–320 . doi : 10.1093/comjnl/ 6.4.308 .

[poly-variadic-5] "Combinadores de punto fijo polivariádicos más simples para recursión mutua" .

[ 1 ]

[ 2 ]

[ 3 ]

[

[ 5 ],