[PL-sem-jr] PL Junior 10/17/2017

[Tony Garnock-Jones]

On 10/11/2017 08:17 PM, Celeste Hollenbeck wrote:
> We are going to talk more about the Y Combinator: What is it? How does
> it work? (For real, this time.)

I learned a lot about y combinators by studying their encodings into pi
calculi (!).

For those with an interest in pi calculi:

There are many encodings of cbn and cbv lambda-calculus in various pi
calculus dialects.

Pick a simple pi calculus, perhaps the synchronous calculus of section 2
of Milner's "The Polyadic $\pi$-calculus: A tutorial" (1991), which
includes a notion of a replicated process, !P.

Pick an encoding of cbn or cbv lambda-calculus into pi.

 1. Write down the encoding of a y combinator.

 2. What role does replication play in the term you have written?

 3. Remove replication from your pi calculus dialect.

 4. Repeat exercise (1) in your reduced dialect.
    Y won't y work now? What has changed?

 5. Can you come up with a revised lambda encoding into your reduced
    pi dialect that works for some lambda expressions?
    What characterises these expressions? Hint: linear logic.

 6. Removing replication was subtle in some ways but embarrassingly
    blatant in others. Are there other large changes you can make to the
    pi calculus that let you retain interesting fragments? Are there
    any other small changes that cripple the language irreparably?

I have some redex models of various pi calculi if anyone wants to play
with them.

Cheers,
  Tony