We present, for the equational theory of a variant of typed λ-calculus, a
method to find interesting conjectures and to design their proofs. Like the
methods taught in basic arithmetic, for the most part the practitioners, which
we imagine as undergraduate or even high-school students, can just follow the
rules but, if they want to, they can apply an intuitive jump at any point without
compromising the outcome. More specifically, we present a series of rules which
allow the student to discover, say, the type of lists, discover that the function
that reverses a list is interesting, discover that the reverse function is its own
inverse and prove so, in much the same way in which they solve a second degree
equation. We maintain a firm conceptual grasp of the method by formalizing it
as a computer program. Such formalization allows us to establish properties of
the method with certainty, first by doing experiments and, in some future work,
by doing Mathematics over the method itself.
Hi again, I am still interested in this topic.
--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/402a4007-b17f-4225-802f-8ccdb1b21c2fo%40googlegroups.com.