Skip to main content
added additional references
Source Link

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:

  • Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:

Knuth's diagram for <span class=$(\lambda y.\lambda z.yz)x$" />

This kind of graphical representation of lambda terms was also studied independently (and more deeply) in two theses in the early 1970s, both by Christopher Wadsworth (1971, Semantics and Pragmatics of the Lambda-Calculus) and by Richard Statman (1974, Structural Complexity of Proofs). Nowadays, such diagrams are often referred to as "λ-graphs" (see for example this paper).

Observe that the above term in Knuth's diagram is linear (inlinear, in the sense that every free or bound variable occurs exactly once) -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:

  • Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:

Knuth's diagram for <span class=$(\lambda y.\lambda z.yz)x$" />

Observe that the above term is linear (in the sense that every free or bound variable occurs exactly once) -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:

  • Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:

Knuth's diagram for <span class=$(\lambda y.\lambda z.yz)x$" />

This kind of graphical representation of lambda terms was also studied independently (and more deeply) in two theses in the early 1970s, both by Christopher Wadsworth (1971, Semantics and Pragmatics of the Lambda-Calculus) and by Richard Statman (1974, Structural Complexity of Proofs). Nowadays, such diagrams are often referred to as "λ-graphs" (see for example this paper).

Observe that the term in Knuth's diagram is linear, in the sense that every free or bound variable occurs exactly once -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).

Source Link

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments.

To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, but the earliest place where I saw it for lambda terms was in an old essay by Knuth:

  • Donald Knuth (1970). Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

On page 234, he drew the following diagram (which he called an "information structure") representing the term $(\lambda y.\lambda z.yz)x$:

Knuth's diagram for <span class=$(\lambda y.\lambda z.yz)x$" />

Observe that the above term is linear (in the sense that every free or bound variable occurs exactly once) -- as others have mentioned, there are non-trivial issues and choices to be made in trying to extend this kind of representation to non-linear terms.

On the other hand, for linear terms I think it's great! Linearity precludes the need for copying, and so you get both $\alpha$-equivalence and substitution "for free". These are the same advantages as HOAS, and I actually agree with Rodolphe Lepigre that there is a connection (if not exactly an equivalence) between the two forms of representation: there is a sense in which these graphical structures may be naturally interpreted as string diagrams, representing endomorphisms of a reflexive object in a compact closed bicategory (I gave a brief explanation of that here).