Upgrade to Pro — share decks privately, control downloads, hide ads and more …

On the Expressive Power of Programming Language...

On the Expressive Power of Programming Languages by Shriram Krishnamurthi

Papers are like poems. Some are dazzling, some are pedestrian, some are insightful, and some reward long periods of quiet contemplation. They stir up an emotional reaction that goes beyond the strictly rational, and can often be deeply personal.

In graduate school, during a period of identity crisis, I came across Matthias Felleisen's “On the Expressive Power of Programming Languages”. At a time when the world was ruled by C++, I had immersed myself in Scheme, so I always looked skeptically at mainstream linguistic claims. However, the language wars seemed beyond rational discourse. So the idea that someone could take a concept as nebulous as "expressiveness" and formalize it was already a revelation. But the beauty of this paper goes well beyond that: it also lies in the cleanliness of the approach, the correspondence of the formalism to intuition, and the tautness of its execution.

It was the most stunning paper I had ever read, and remains so. It's like the poem that never leaves your soul.

Unfortunately, this paper may not be easy to read for the uninitiated: it depends on a certain amount of “cultural knowledge” of programming language theory. I hope to peel off some of those layers and help you, too, understand the paper — hopefully while preserving the joy and beauty I experienced.

Papers_We_Love

September 12, 2019
Tweet

More Decks by Papers_We_Love

Other Decks in Programming

Transcript

  1. What is this paper about? We have sharp, mathematical distinctions

    between some classes of language features These offer advice to language designers Beyond a point (the “Turing Threshold”), we have none…
  2. Intuition: something about compilation If we can translate/compile L +

    F down to L, F is probably not expressive…
  3. Better intuition: local translation “local” means “nobody else needs to

    know” Essentially, simple Lispy macro systems (The Las Vegas principle) (for i lo hi body) è (define i lo) (while (< i hi) body (increment i))
  4. x + 2 [x*x | x <- l] x or

    y x.__add__(2) map (\x -> x*x) l let t = x in if t then t else y
  5. When a macro for F to L exists! Given semantics

    for L and L + F, for all programs P in L + F: say PL (in L) is the result of “expanding” F then P (in L + F) is “equal” to PL (in L)
  6. Need to show that no macro can possibly exist That

    is the interesting part of this paper! Both parts rely on a definition of “equality”
  7. Equality is hard… Counterpoint: equality is easy! For two expressions

    e1 and e2 , run(e1 ) à v1 run(e2 ) à v2 compare v1 and v2
  8. Observational equivalence Is there a way in the language of

    telling the two answers apart? If so, some program might use it!
  9. E :: = v | c | (op E …)

    | (E E …) | (λ (v …) E) A context C[•] is an expression E with some sub-expression replaced with a • (+ 1 •) (f x • y) (λ (x) (+ x •)) What are all the ways of using a piece of code in a program? We’ll treat ourselves to more language…
  10. For all contexts C, if C[e1 ] = C[e2 ],

    e1 ≅ e2 Can you in code (i.e., with a context): • … tell apart 1 and 0.999…? • … inspect program source? • … measure time/power? more “observations” è fewer equivalences
  11. Even more general definition: e1 ≅ e2 if, for all

    contexts C, C[e1 ] halts iff C[e2 ] halts A small “trick”: programs with errors don’t terminate Ω is a canonical non-terminating term
  12. e1 ≅A e2 if, for all contexts C in language

    A, C[e1 ] halts iff C[e2 ] halts
  13. Is this okay? Doesn’t this imply 5 ≅ 6? C[•]

    ≜ (if (=? • 5) “halt” Ω) The definition is for all contexts, and that’s one of ’em!
  14. What if the language doesn’t have any way of telling

    5 and 6 apart? What if (=? • 5) is not a language operation? Maybe it has only 0? C[•] ≜ (if (0? (- • 5)) “halt” Ω)
  15. Motivation for the definition Suppose we have 3 ≅L (+

    1 2) Could adding F0 leave 3 ≅L + F0 (+ 1 2)? Could an F1 leave all ≅L pairs ≅L + F1 ? Could adding F2 make 3 ≆L + F2 (+ 1 2)?
  16. Key Theorem Suppose F can be written as a local

    macro Then for all e1 and e2 such that e1 ≅L e2 , e1 ≅L + F e2 That is, F has not added power to L
  17. How to show expressiveness? Start with L terms e1 and

    e2 such that e1 ≅L e2 If we can find a C in L + F that can distinguish e1 from e2 (i.e., e1 ≆L + F e2 ) Then, F has added power to L (and can’t be expressed as a local macro)
  18. Reminder Start with L terms e1 and e2 such that

    e1 ≅L e2 If we can find a C in L + halt that can distinguish e1 from e2 (i.e., e1 ≆L + halt e2 ) …
  19. e1 ≜ (λ (f) Ω) e2 ≜ (λ (f) ((f

    0) Ω)) C[•] ≜ (• halt) C[e2 ] = 0 C[e1 ] = Ω
  20. e1 ≜ (λ (f) Ω) e2 ≜ (λ (f) ((f

    0) Ω)) C[•] ≜ (call/cc •) C[e2 ] = 0 C[e1 ] = Ω
  21. e1 ≜ (λ (_) (f 0)) e2 ≜ (λ (_)

    (f 0) (f 0)) C[e2 ] = Ω C[e1 ] = 0 C[•] ≜ (define (f x) (set! f (λ (_) Ω)) x)) (• 0) take a parameter and return it changing f to a diverging function
  22. Semantics of Lif: (Lif #f A B) à B (Lif

    <any other value> A B) à A (Similar argument for other truthy/falsy)
  23. e1 ≜ (Bif (p (λ () Ω)) (Bif (p #f)

    0 1) Ω) e2 ≜ The same term but with 1 replaced by Ω C[•] ≜ (define p (λ (x) (Lif x #t #f))) • C[e2 ] = Ω C[e1 ] = 1 p is not a procedure p applies its arg p does arith its arg p Bif’s its arg p ignores its arg
  24. Local vs global transformations pure language + state: store-passing style

    control operators: continuation-passing style They can’t be local transformations They do add expressive power
  25. What have we learned? A beautiful, practical definition of equality

    A clever definition of expressiveness Proof sketches that show us it matches intuition
  26. What else is in the paper? Multiple notions of expressiveness

    Proof of that theorem (not trivial at all!) Relationship to logic Relationship to other formalizations
  27. Implications for language design Desugaring/macros are now everywhere Macros can

    have a variety of powers Allowing macros that increase expressiveness… is something to be done with care