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)) ... )
===> 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? ) that returns
#t if ( ) 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) -->
(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)?
------------------------------------------------------------------------