Usage Notes

System.Exception: Unparsed input

Currently the parse function cannot handle text followed by end-of-line and will produce a parse error. The solution is to use a verbatim string by placing a @ before the string. e.g. @"some text is a string"

Union-find algorithm

In lib.fs

See: Disjoint-set data structure
See: Topics in Automated Deduction - Lecture 5 - Page 4: Union/Find
union is called equate.
find is called canonize.

Reasons for stack overflows

Example is to show that result will not converge.
F# does not optimize code as well as OCaml so some code in F# does not become a tail call.
F# has only 1 meg for stack and OCaml has more.

Debug a single example

One effective way to debug a single example in one of the fsx files is

In Visual Studio F# Interactive window, right click, Reset Session
In Visual Studio F# Solution Explorer under Examples, open init_all.fsx
In init_all.fsx, select all, right click, Send To Interactive
Set your break point(s) in Visual Studio.
Using VS menu: Tools -> Attack to Process..
Double click process: Fsi.exe
With mouse, select example statement you want to debug, right click, Send To Interactive.

You should be at your first break point.

Books and papers used for examples

K&B - Knuth, D. E. and Bendix, P. (1970) Simple word problems in universal algebras. In Leech. J. (ed.). Computational Problems in Abstract Algebra. Pergamon Press.

Baader & Nipkow - Baader, F. and Nipkow, T. (1988) Term Rewriting and All That. Cambridge University Press.

Pelletier - Pelletier, F. J. (1986) Seventy-Five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning , 2 191-216. (C) 1986 by D. Reidel Publishing Company. Errata, JAR 4 (1988), 235-236

Dijkstra (1989) - On an exercise of Tony Hoare's.

Dijkstra (1997) - Proving an implication via its converse.

Prasetya (1993) - info-hol archive 18 Oct 1993