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.

Transcript

1. Presented by Shriram Krishnamurthi Brown University
2. 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…
3. A Little Personal History
5. What’s Expressive?
6. L + F
7. Loop/Function-Free Language + Loops
8. while language + for
9. for language + while
10. Regular language + Context-free grammar
11. Two-Armed if + Multi-Armed if
12. Pure Language + State
13. Language w/ binary – + Unary –
14. Language w/out Exceptions + halt
15. Does F add expressive power to L? L L + F
16. Intuition: something about compilation If we can translate/compile L + F down to L, F is probably not expressive…
17. JavaScript x86 (Church) (Turing)
18. The genius of this paper: Extracting us from the “Turing tar-pit” (Perlis)
19. 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))
20. 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
21. Two Sides of Expressiveness
22. When is F not expressive relative to L? L L + F
23. 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)
24. When is F expressive relative to L? L L + F
25. 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”
26. Equality is Hard
27. But first… * “closed terms” “capture-free substitution” “program contexts”
28. Equality is hard… Counterpoint: equality is easy! For two expressions e1 and e2 , run(e1 ) à v1 run(e2 ) à v2 compare v1 and v2
29. Comparing as strings What about 1 and 0.9999999…?
30. What about functions? (λ (x) (* 2 x)) (λ (x) (+ x x))
31. What about free variables? (* x 3) (+ x x x)
32. What about closures? Not just code, also environments, etc.
33. What if you can measure running time? power consumption? …
34. These aren’t just #TheoryWorldProblems… Every compiler optimization needs to replace terms with ones “equal” to them
35. Observational equivalence Is there a way in the language of telling the two answers apart? If so, some program might use it!
36. 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…
37. 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
38. 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
39. e1 ≅A e2 if, for all contexts C in language A, C[e1 ] halts iff C[e2 ] halts
40. 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!
41. 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” Ω)
42. Back to Expressiveness!
43. 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)?
44. 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
46. 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)
47. Language w/out Exceptions + halt
48. 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 ) …
49. e1 ≜ (λ (f) Ω) e2 ≜ (λ (f) ((f 0) Ω)) C[•] ≜ (• halt) C[e2 ] = 0 C[e1 ] = Ω
50. e1 ≜ (λ (f) Ω) e2 ≜ (λ (f) ((f 0) Ω)) C[•] ≜ (call/cc •) C[e2 ] = 0 C[e1 ] = Ω
51. Pure Language + State
52. 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
53. Pure w/ Boolean-only if (Bif) + Truthy/Falsy if (Lif)
54. Semantics of Lif: (Lif #f A B) à B (Lif <any other value> A B) à A (Similar argument for other truthy/falsy)
55. 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
56. 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
57. Wrapping Up
58. What have we learned? A beautiful, practical definition of equality A clever definition of expressiveness Proof sketches that show us it matches intuition
59. 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
60. 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
61. Benefits of expressive features Avoids non-local/global transformation Greater modularity otherwise Patterns…which can be misused Patterns…which hide intent
62. Homework Is the with construct of JavaScript expressive w.r.t. the rest of JavaScript?
63. Homework Is the generator construct of Python expressive w.r.t. the rest of Python?