recitation 23: static analysis & the halting problem

------------------------------------------------------------------------
evaluator for a language designer (change the syntax/semantics)
evaluator for theoretician (what is computable?)

------------------------------------------------------------------------
analyze evaluator:  split eval into two parts, 
  1. syntactic (static) analysis of expression:  "do something now"
  2. evaluation of an execution procedure:  later we'll "complete the evaluation"

analyze: expression -> EP
EP (execution procedure): environment -> anytype 

why would we want to perform static analysis?
  * improve execution performance
     - avoid repeated work (avoid repeated parsing)
  * catch bugs early 
     - type checking, # of arguments, etc
  * prove things about program
     - time/memory usage

------------------------------------------------------------------------
* can we extend the analyze evaluator to detect expressions which have
  side effects (mutation or printing to the screen)?  how?

* can we extend the analyze evaluator to determine the free variables
  in a particular expression?  (what are free variables?)  how?

* can we extend the analyze evaluator to check for undeclared
  variables statically?  how?

  (analyze '(let ((x 2)) (+ x y)) ... <other args?> )
    ===> warning: evaluation will result in "unbound variable y" error

* can we extend the analyze evaluator to check for other types of
  errors (wrong # of arguments, wrong types of arguments, divide by
  zero, ... )?  how?

------------------------------------------------------------------------
universal machine: something that can "reconfigure itself" to look
  like any particular machine

notion of computability: anything computable in one language is also
  computable in any other language

------------------------------------------------------------------------
is everything computable?  what's the halting problem?  (from sicp ex 4.15)

* can you define a procedure (halts? <program> <input>) that returns
  #t if (<program> <input>) halts (returns a value) and #f if it results
  in an error or an infinite loop?

  (define (run-forever) (run-forever))
  (define (halt-dummy x) 'done)
  (define (run-forever-dummy x) (run-forever))

  (run-forever)                --> <infinite loop>
  (halts? halt-dummy 1)        --> #t
  (halts? run-forever-dummy 1) --> #f

ok, once halts? has been defined, let's do:

  (define (try p)
    (if (halts? p p)
	(run-forever)
	'halted))

* what happens when we evaluate (try halt-dummy)?
* what happens when we evaluate (try run-forever-dummy)?
* what happens when we evaluate (try try)?

------------------------------------------------------------------------