¿Cuál es el beneficio de la notación de Krivine?

9

Vi que algunas personas usan la notación de Krivine para la aplicación de funciones cuando presentan la sintaxis para el cálculo . Por ejemplo, el λ -term λ f . λ x . λ y . f x y (con la convención normal de que la aplicación de función se asocia a la izquierda, por lo que en realidad significa que λ f . λ x . λ y . ( ( f x ) y ) ) se escribe λ f . λ x . λ yλλλf.λx.λy.f x yλf.λx.λy.((f x) y) (con una convención similar que en realidad significa λ f . λ x . λ y . ( ( f ) x ) y ). No veo el punto de tener otro par de paréntesis alrededor del f más interno. ¿Por qué las personas usan la notación de Krivine en lugar de la habitual?λf.λx.λy.(f) x yλf.λx.λy.((f) x) yf

día
fuente

Respuestas:

13

Supongo que te refieres a la notación de Krivine del cálculo Lambda: tipos y modelos .

Esta notación, utilizada como representación de datos, hace que muchos algoritmos en términos lambda sean más simples de implementar y resulten correctos. Es decir, dado un término lambda , desea verlo como unacabeza f , junto con unalistade argumentos [ e 1 , e 2 , ... , e n ] .fe1e2en f[e1,e2,,en]

Por ejemplo, suponga que desea comparar dos términos con gfe1en . A menudo es más natural comparar las cabezas f y g primero, y ni siquiera mirar los pares ( e i , t i ) a menos que esa comparación tenga éxito. (Esto a menudo aparece en implementaciones de unificación de orden superior).gt1tnfg(ei,ti)

Vea el artículo de Cervesato y Pfenning A Linear Spine Calculus para una formalización de esta idea.

Neel Krishnaswami
fuente
0

Una diferencia interesante aparece en la Sección 2 "Funciones representables" del Capítulo 2 del libro de Krivine. Iglesia codificada tres se escribe en notación estándar como λ x. λ y. x (x (x y)) . Con la notación de Krivine (si finalmente lo estoy entendiendo correctamente), en su lugar escribiríamos λx λy (x)(x)(x)y .

Aaron Stump
fuente