Help with Herbelin

DISCLAIMER: I'm uneducated with PLT and don't know what I'm talking about, so please forgive any whacked terminology.

Ok, that outta the way...

I'm trying to make my way through The Duality of Computation (https://pdfs.semanticscholar.org/048f/c94be2ec752bb210c5f688cba0200c1a1f92.pdf), and this stuff, like most everything posted on this fascinating website, is way over my head. I can't follow most of the back half of the paper, but I was hoping someone might have the spare time to answer two newbie, school-level, questions...

1) (The silly one.) How on earth do you pronounce the "mu, mu with tilde" calculus. It'd literally be easier to read this if I knew how to read it. Is there some definitive guide for people who just figured out that the funny squiggle so many these papers is pronounced "eta"? :)

2) (The basic one.) The authors talk about the call-by-value side of the duality as dealing with "Environments with holes." This reminds me of PTS, with it's capital-PI lambda expressions that can close over terms or types. What's the difference between an "Environment with a hole" and a lambda over environments? And what does that mean for compiled languages, where environments aren't parameters?

Any help on either question would be appreciated.

waltzing Matilda

Looks like (1) may be pronounced "moo moo til duh", since I see papers that spell out phrases like lambda-bar-mu-mu-tilde with hyphens, just like that, which suggests people actually say this. The last three syllables might sound like Matilda if said quickly.

By Rys McCusker at Wed, 2017-10-04 22:57 | login or register to post comments

:)

By jimdesu at Thu, 2017-10-05 01:58 | login or register to post comments

myoo

I learned (perhaps from my father?) to pronounce "mu" as "myoo" (same as English "mew").

By John Shutt at Thu, 2017-10-05 02:00 | login or register to post comments

thanks

Funny you should answer... how 'bout "vau"? :P

By jimdesu at Thu, 2017-10-05 03:34 | login or register to post comments

Good question

When I started working with vau, I had no clue how to pronounce it. I didn't know better than to pronounce the initial consonant as that of English "vow", and I'd never been sure whether to pronounce tau to rhyme with "paw" or "pow". I developed a habit of ignorant pronunciation that I now can't seem to shake. However, I've since been told by Shriram Krishnamurthi that the proper Greek pronunciation is "wow" (just as the English word). There's a meme floating around, which I speculate originates from Shriram, calling vau "the wow combinator".

By John Shutt at Thu, 2017-10-05 04:21 | login or register to post comments

environments with holes

I know mu-mutilda, but not what you mean by "environment with hole". There are several things that could be what you mean:

Evaluation contexts in traditional syntactic lambda-calculus presentation are traditionally written with a hole where the evaluated value should be plugged, `E[]` or `E[□]`. The paper sometimes speaks of "(evaluation) contexts with a hole".

The syntactic category of "contexts" in this paper, using the same metavariable `E`, is different from the standard notion of context above, but isomorphic: it is a concrete syntax to represent an evaluation context as a concrete datastructure, as an explicit part of the program representation. The paper sometimes implicitly relates the two notions.
The construction `mutilda x. c` binds a variable `x` within a command `c`, and the whole thing is a context (sometimes called a "co-term", as the syntactic category of context is what is opposite to terms, their dual). It is essential to modelling call-by-value in mu-mutilda.

`mutilda` is a binder, like `lambda`, so in this sense they are similar. `mu` and `mutilda` could be seen as "more atomic" than lambda, and in fact it possible to represent `lambda` as a derived form expressed in term of a variant of `mu` -- but this is easier to see when you read papers about mu-multida that have more connectives/datatypes than just functions, so not in this paper.
The judgment `Gamma | E : A |- B` is non-standard syntax (if you are only familiar with type system with lambda-calculi), and the new position `| E : A` might be thought of a "hole" in a *typing environment* Gamma (or typing context). I don't think "hole" is used in this way in the paper, even if it makes some sort of sense (if `Gamma | E : A |- B` holds, then E corresponds to a traditional evaluation context E[□] that, if a term `t : A` is plugged in it, gives a term `E[t] : B`. But the better way to think of this judgment is that `E` is a co-term that "consumes" an `A` to behave as a command `Gamma |- B`.
In Section 9 of the paper, "head reduction in an abstract machine", *dynamic* environments are discussed (and vaguely relevant to a discussion of interpretation vs. compilation), but not with holes. I think this section is a bit too complex and not hugely important, you may safely skip it on first read.

By gasche at Thu, 2017-10-05 07:49 | login or register to post comments

hmmm

So, maybe I've misunderstood -- I've been interpreting "evaluation context" as the environment in which terms are denoted. So if you have an "A : T", that's true because the context contains an A of that type. In the few interpreters I've written, I've always passed environments implicitly (generally using a "spaghetti stack"). But from what you're saying that seems to be wrong. Is "evaluation context" more like the surrounding/enclosing term of the term being discussed?

(My category theory's really weak, so I'm lost on the co-term bit, but I'll work on that.)

By jimdesu at Fri, 2017-10-06 17:07 | login or register to post comments

Evaluation context

The notion of evaluation context in works about the lambda-calculus is different from what you think (I think), simple, elegant, and absolutely standard in the field (it's a prerequisite for reading most research articles). In terms of low-level implementations, it corresponds to a combination of the program counter and the call stack (exactly what you need to save to capture a non-delimited continuation, if that speaks to you), but the way it is defined and we think about it is much simpler and it will really help you to familiarize yourself with this notion first.

Googling for "small-step operational semantics" gives results as course notes, most of which present evaluation contexts. I don't remember where I learned about them myself, possibly from the Core ML chapter of the available-online book " Using, Understanding, and Unraveling The OCaml Language -- From Practice to Theory and vice versa".

The original research papers that introduces evaluation contexts, I think (edit: this is wrong, see shriramk's reply below), is "A syntactic approach to type soundness", Andrew Wright and Matthias Felleisen, 1994, but it uses them to solve a harder problem and discusses a lot of the scientific literature of the time, which is interesting (and mostly still relevant) but not on the shortest path to you understanding contexts.

By gasche at Fri, 2017-10-06 18:20 | login or register to post comments

thanks

much appreciated

By jimdesu at Fri, 2017-10-06 22:31 | login or register to post comments

earlier than that

Almost everything about this post is right on except the statement about the paper that introduced the idea. It was introduced principally in Felleisen's thesis, and in some of the papers leading up to that document. Felleisen and Hieb's magnum opus is generally the canonical reference.

A more modern presentation is in the PLT Redex book. This may be a useful introduction to someone trying to understand what an evaluation context is:

https://redex.racket-lang.org/why-redex.html

By shriramk at Thu, 2017-12-21 14:48 | login or register to post comments

Thanks

Noted, thanks!

By gasche at Thu, 2017-12-21 16:01 | login or register to post comments

thanks y'all

eventually I'll understand this stuff :)

By jimdesu at Fri, 2017-10-06 22:30 | login or register to post comments

Lambda the Ultimate

User login

Navigation