> I wonder why not *apply* these interesting and generalized Scheme > discussions to the comp.lang.scheme newsgroups? I've CC'ed comp.lang.scheme.
> 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). Would you need records, though? Otherwise what would you "theorem?" predicate look like? Or wouldn't you need such a predicate? > Besides, I don't think records in Scheme are all that static, at least > not if not truly builtin. I'm not sure whether I care about the static/dynamic difference... mostly because I don't know the tradeoffs. Presumably you can be faster if you're static. The proposal I made of hiding the privileged constructors of a theorem record in a library wouldn't amount to adding static type checking to Scheme at all, but it might be a way to guarantee the soundness of the theorems without any overhead compared to ML. (I might be wrong... let me know.) > > 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. >> >
