Friday 28 December 2012

That damn halting problem

I'm fixing my gEDA fork so that it will work with Guile 2.0. There are several good reasons for doing so, including moving with the times and hopefully cleaner valgrind output. There's an interesting new feature in this new major release of Guile: scheme source files get compiled automatically. (They get cached under $HOME/.cache/guile, in case you're wondering.)

All that cleverness presumably leads to faster-running code (at the cost of slower startup), but it also results in this output to stderr:


;;; compiling /usr/local/geda/share/gEDA/system-gafrc
;;; /usr/local/geda/share/gEDA/system-gafrc:31:18: warning: possibly unbound variable `build-path'
;;; /usr/local/geda/share/gEDA/system-gafrc:40:24: warning: possibly unbound variable `build-path'
;;; /usr/local/geda/share/gEDA/system-gafrc:43:0: warning: possibly unbound variable `load-scheme-dir'
;;; /usr/local/geda/share/gEDA/system-gafrc:48:19: warning: possibly unbound variable `build-path'
;;; compiled /home/berndj/.cache/guile/ccache/2.0-LE-8-2.0/usr/local/geda/share/gEDA/system-gafrc.go
;;; compiling /usr/local/geda/share/gEDA/scheme/geda.scm
;;; compiled /home/berndj/.cache/guile/ccache/2.0-LE-8-2.0/usr/local/geda/share/gEDA/scheme/geda.scm.go

system-gafrc loads geda.scm with a call to (load-from-path "geda.scm") that occurs before the first use of build-path or load-scheme-dir. Unfortunately, the compiler can't "see through" the call to load-from-path, and hence can't see that geda.scm provides the definitions of the functions system-gafrc calls.

The compiler can't see through these calls in the general case because to do so would be to solve the halting problem. Just imagine that just above the call to (load-from-path "geda.scm") were a chunk of code that wrote a definition for build-path if and only if it searched ℤ3 and found a triple such that x3 + y3 = z3. We know now (thanks, Andrew Wiles) that this is impossible, so substitute a search based on any other as yet unproven conjecture, if you like. (This is a counter to the objection of the student (my younger self included) to the impossibility of solving the halting problem: "But I can show that these programs halt!")

And that is why it isn't reasonable to expect guile's auto-compiler to know that build-path and load-scheme-dir are, in fact, defined before use. That's a separate matter from whether it should warn or not.