I wonder why not *apply* these interesting and generalized Scheme discussions to the comp.lang.scheme newsgroups?
Anyway, I think you're confusing static and dynamic type checking. Sure it's possible to write theorem provers in pure R5RS Scheme by relying on predicate functions and dynamic type checking. I think the so-called soft-type checkers for Scheme were like that -- they are theorem provers trying to validate a scheme program as input (supposed theorem). Besides, I don't think records in Scheme are all that static, at least not if not truly builtin. On Wed, May 27, 2009 at 5:02 PM, Ramana Kumar <[email protected]> wrote: > Interactive theorem provers like HOL and Isabelle use the static type > checking in ML, where type safety is guaranteed, to guarantee > soundness. Specifically, something of type "thm" (for theorem) must be > true, because (I think this is how it works) only the axioms and > inferences rules produces things of that type. At the same time, these > systems are very extensible and you can write more powerful inference > rules or functions that return theorems in ML... the type system > ensures that the only way these functions can work is by proving their > results, i.e. calling the low level axioms and rules. > > Now I've been thinking about whether one could write something like > HOL in Scheme. At the moment I'm thinking you could put the kernel > (the axioms and inference rules) in a library along with a new theorem > record type, and then not export any method for creating theorem > records that isn't an axiom or rule. Would that guarantee soundness in > the same way, or can you never really restrict how records of a type > are created? Also, is it possible to do it without records or > libraries (e.g. in R5RS)? Finally, let me know if there already exist > theorem provers written in Scheme. >
