Lambda the Ultimate

inactiveTopic Using an Abstracted Interpreter to Understand Abstract Interpretation
started 8/27/2003; 1:51:45 AM - last post 9/5/2003; 10:54:30 AM
Ehud Lamm - Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 1:51:45 AM (reads: 9692, responses: 20)
Using an Abstracted Interpreter to Understand Abstract Interpretation
(postscript version)

Another great learning resource from Dan Friedman.

As you'd expect, we have a hands-on practical tutorial on AI.

The code is in Scheme, of course.

Enjoy!


Posted to general by Ehud Lamm on 8/27/03; 1:53:34 AM

Dominic Fox - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 12:19:35 PM (reads: 1414, responses: 1)
Enjoy!

Or: would you like fries with that?

The Seasoned Schemer arrived on my doorstep this morning. As I've said before, I don't mind the pedagogical style too much. I do find that it slows me down, but that's not altogether a bad thing.

Having said that, I've found some of Graham Hutton and Erik Meijer's short introductory papers on things like folds, parser combinators and so on extremely well-paced and readable; and I don't think the paper linked to here suffers in the least from not being essayed in pseudo-socratic style. Sometimes it's nice to just get on with it.

Ehud Lamm - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 12:42:57 PM (reads: 1437, responses: 0)
I am not sure I understand. "Sometimes it's nice to just get on with it", is a compliment?

I love Dan's style and his tutorials (the Poorman's series) are great. The Little Schemer, though, isn't one of my favorites. De gustibus and so on..

Michael Vanier - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 1:00:52 PM (reads: 1422, responses: 1)
I love "The Little Schemer" ;-) I particularly like the way they (Dan and Matthias) go from elementary concepts up to really tricky stuff like the Y combinator. In fact, I *still* don't completely get their explanation of Y, but I *almost* do.

Ehud Lamm - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 1:09:24 PM (reads: 1435, responses: 0)
This is one of the things that bug me. Sure, it's Socratic and all, but when things become tricky, you either get them or you don't. The Q&A format doesn't make understanding these things easier.

When I first read TLS, I was stuck with the Y combinator, drew all kinds of craxy diagrams (I didn't know any useful technique, nor did I understand environments and such), but didn't really understand what's going on. When I finally understood fixed points (or at least stopped being mortally afraid of them) it was with the help of more in depth and wordier explanations.

We should distinguish between the Q&A format, with ultra-short questions and answers, from the more fundamental property of Dan and Matthias's approach: hands on, with fully executable code presented at every step along the way. That's also what makes EOPL and EOPL2 so enlightening.

Vesa Karvonen - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 2:23:33 PM (reads: 1412, responses: 0)
In fact, I *still* don't completely get their explanation of Y, but I *almost* do.

Speaking of the Y combinator, I think that the most effective way to begin to understand the Y combinator is to actually derive and implement it by yourself (you'll probably want to use a dynamically typed language). Once you have derived (and understood the derivation) the Y combinator by yourself, it becomes much easier to follow any discussion that talks about it.

Here is how you can derive a fixed point combinator in a strict language such as Scheme.

1. Start from a simple recursive function:

(define rec-factorial
  (lambda (n)
    (if (= 0 n)
        1
        (* n (rec-factorial (- n 1))))))

(rec-factorial 5) ==> 120

2. Parameterize the function by self in order to eliminate direct reference to self:

(define self-factorial
  (lambda (self)
    (lambda (n)
      (if (= 0 n)
          1
          (* n ((self self) (- n 1)))))))

((self-factorial self-factorial) 5) ==> 120

3. Move the (self self) application to a Y-combinator:

(define Y-factorial
  (lambda (self)
    (lambda (n)
      (if (= 0 n)
          1
          (* n (self (- n 1)))))))

(define Y (lambda (f) (f (lambda (n) ((Y f) n)))))

((Y Y-factorial) 5) ==> 120

Question: What happens if you perform an eta-reduction on the second lambda in the above definition of Y?

4. Finally remove the reference to self from the Y combinator. I'll leave this as an exercise. (Hint: Use the same technique as in the second step.)

Suraj Acharya - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 4:14:09 PM (reads: 1380, responses: 0)
"The Why of Y" by Richard Gabriel is what helped me finally wrap my brain across the Y combinator. It follows the same reasoning as Vesa's post above with a lot more textual exposition.

http://www.dreamsongs.com/NewFiles/WhyOfY.pdf

I'm posting it here because according to the google search the article has not been referenced here before.

Tayssir John Gabbour - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/27/2003; 7:23:31 PM (reads: 1376, responses: 1)
Speaking of Y-combinator, André van Meulebrouck wrote a really impressive set of tutorials that I stumbled upon when looking around for lisp knowledge.

http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/index.html http://www.mactech.com/articles/mactech/Vol.08/08.01/DazeY/index.html

The first link has the Y-combinator at the bottom, first in normal form, then in the lispy applicative form. There are other similar articles by him on the Mactech site.

Ehud Lamm - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/28/2003; 12:11:18 AM (reads: 1340, responses: 0)
Another useful read concerning Y.

Michael Vanier - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/28/2003; 2:00:30 AM (reads: 1289, responses: 0)
You guys are awesome! Thanks for the explanations and links!

Vesa Karvonen - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/28/2003; 2:58:38 AM (reads: 1288, responses: 0)
If we would characterize the previous derivation of the Y combinator as top-down design, then we might ask how to derive the Y combinator using bottom-up design.

1. Start from a divergent expression.

(define divergent
  (let ((diverge (lambda (self)
                   (self self))))
    (diverge diverge)))

The above results in an infinite process. How could we make use of it? This is the essential bottom-up step: ask how to make use of some primitive building block.

2. Find a way to parameterize the infinite process with a function that does useful work.

Probably the easiest way is to start with a side-effecting procedure rather than a pure function.

(define display-1
  (lambda ()
    (display 1)))

(define p-divergent (lambda (p) (let ((diverge (lambda (self) (p) (self self)))) (diverge diverge))))

(p-divergent display-1) ==> 111111111111111111111111111111...

How could we stop the process?

3. Parameterize the procedure with the process so that the procedure can control the process.

(define counter 10)
(define display-10x1
  (lambda (continue)
    (if (< 0 counter)
        (begin
          (display 1)
          (set! counter (- counter 1))
          (continue)))))

(define se-fix (lambda (pc) (let ((se-fix (lambda (self) (pc (lambda () (self self)))))) (se-fix se-fix))))

(se-fix display-10x1) ==> 1111111111

Does this remind you of CPS?

How do we get rid of the ugly side-effects?

4. Parameterize the procedure with state so that the procedure does not have to use side-effects to control the process.

(define display-Nx1
  (lambda (continue)
    (lambda (N)
      (if (< 0 N)
          (begin
            (display 1)
            (continue (- n 1)))))))

(define fix (lambda (f) (let ((fix (lambda (self) (lambda (s) ((f (lambda (s) ((self self) s))) s))))) (fix fix))))

((fix display-Nx1) 10) ==> 1111111111

And we have actually arrived at the fixed point Y combinator.

Ehud Lamm - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/30/2003; 2:05:44 PM (reads: 1074, responses: 0)
How about discussing the abstract interpreter (and AI theory) presented by Friedman?

It's an important topic that for some reason isn't discussed often on LtU.

ferix - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/31/2003; 2:54:30 PM (reads: 1021, responses: 1)
I would discuss the interpreter, but I haven't finished reading the paper yet.

I got sidetracked exploring the differences between's Friedman's MATCH form, and the MATCH implemented by MzScheme.

I have almost finished porting the Chez Scheme source for Friedman's MATCH over to MzScheme.

But as an obligatory on-topic addition, I'm not sure if I buy the paper's logic that boolean values should map to Bottom, "because they add no information." Call me crazy, but (+ 1 #f) is an erroneous expression; its not positive, negative, or zero. So I would think that the safest thing would be to map booleans to Top.

Patrick Logan - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
8/31/2003; 3:37:05 PM (reads: 1018, responses: 0)
Call me crazy, but (+ 1 #f) is an erroneous expression

Unfortunately in Python 2.3 we'd have to call you crazy.

Regretably, they've really screwed up.

Ehud Lamm - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/1/2003; 12:34:07 AM (reads: 1024, responses: 0)
I would think that the safest thing would be to map booleans to Top.

I am not sure I understand how this will effect the AI.

However, I think that the explanation given "because they add no information," is far from helpful. This is one of the weakest points in the article.

Sjoerd Visscher - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/1/2003; 1:58:04 AM (reads: 991, responses: 2)
What I understood from the article was that Top means an integer with unknown sign, while Bottom means not an integer, error or no termination.

Ehud Lamm - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/1/2003; 2:17:06 AM (reads: 1002, responses: 0)
Top means an integer with unknown sign

To quote the paper: We have too much information to determine the answer. It is ambigous.

Am I the only one who find the phrase "too much information" strnage in this context? I understand what's going on, but I think this sentence can be mighty confusing, if that's the first time you come across this phenomenon.

Sjoerd Visscher - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/1/2003; 6:13:35 AM (reads: 977, responses: 0)
Yes, I found that very strange. I'd say we have not enough information, or else we would have been able to determine the sign.

Maybe it should have said "too many possible answers" (where too many is more than one).

ferix - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/1/2003; 8:44:01 AM (reads: 982, responses: 0)
The problem I see with making error/no-termination equal to Botton, is that (Ds-lub bottom Y) will return Y. Ds-lub is used to evaluate if-expressions; it seems like (if <test> #t 1) will be interpreted as returning a positive integer, not an error.

But, like I said above, I haven't finished porting the match macro over, so I haven't tested Friedman's code, so don't hold me to this conclusion.

Actually, I did finish porting enough of the macro over last night to run all of the code given in the interpreter (I don't think they use patterns of the form "(a ,x ... z)" in the paper), so I'll probably try it out later today and see if it handles these cases properly.

Michael Vanier - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/2/2003; 1:40:52 PM (reads: 906, responses: 0)
This is a very interesting thread.

My interpretation of bottom and top is as follows. Bottom means there is no valid answer. Top means that there is more than one possible valid answer. I agree that this could have been discussed more fully in the paper.

In fact, I found the paper rather rough sledding. I also didn't like how abruptly it ended; I would have liked more discussion about the big picture e.g. about why abstracted interpreters are useful. Still, it was a fascinating read.

claudio - Re: Using an Abstracted Interpreter to Understand Abstract Interpretation  blueArrow
9/5/2003; 10:54:30 AM (reads: 822, responses: 0)
There is a nice introduction about abstract interpretation and static analysis in http://www.cis.ksu.edu/santos/schmidt/Escuela03/