GCD - A Case Study on Lucas-Interpretation.
Walther Neuper · 2014
Lucas-Interpretation [5] combines computation and deduction such that a learner has free choice in interaction while solving problems in applied mathematics: a next step can be requested from the system and/or can be input with feedback from the system. Thus interactive support in stepwise problem solving comes close to traditional paper and pencil work. Next steps are computed by a program, while interpretation works stepwise like in a debugger and maintains an environment together with a logical context. The latter provides automated provers with data to check user input by establishing (or not establishing) deductions of input formulas from the context. The prototype of Lucas-Interpretation in the ISAC project1 raises several open research questions. One of them are the limits of “next-step-guidance”: Which kinds of input guarantee the interpreter to resume execution? So far, there is one positive answer [2], lemma 7 on p.182. Another open question is revealed in the proof of the above mentioned lemma, which involves reachability, not yet tackled in Isabelle [8]: How relates logical consistency of a calculation with the operational semantics of the respective program? Interest on clarification of theoretical foundations for LucasInterpretation is motivated by a case study [7]: this study revealed that ISAC’s programming language is too complicated to hand over authoring to the public. A promising way to make ISAC’s programming language easier to use is to approach Isabelle’s function package [4]. Most urgent for practical use is inclusion of rewriting (see example [5].p.92) into the function package; however, this inclusion will introduce a new class of termination proofs. Another kind of examples are engineering problems like [5].p.85; however, for these examples logical consistency is still unclear: clarification involves operational semantics of the programming language, which has not yet been tackled. The present study investigates a class of examples, which is not affected by either difficulties, neither be rewriting and termination nor by engineering problems with involved semantics.