The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #727

Title:From Meta-Level Tactics to Object-Level Programs
Authors:Horn,C; Smaill,AD
Date:Dec 1994
Presented:In "Artificial Intelligence in Mathematics", J. Johnson et al. (eds), Clarendon Press, Oxford, 1994, pp 135-146
Keywords:
Abstract:The paper describes a variant of Martin-Loef type theory extended by the principle of type induction, as introduced in the oyster-2 theorem proving system. The system has a procedural meta-language in which a variety of search strategies have been written. Theorem proving in the system yields object-level functional programs that implement procedures associated with the theorem that is proved. We demonstrate the application of type induction in proving the existence of a partial decision procedure for a fragmentation of type theory inside the theory itself. As a result of that proof, we obtain an object-level program that implements such a partial decision procedure, ie given a type theoretic formula x as input, it returns either a proof of x (formally, an element of the type x), or a refutation of x (formally, an element of the type x - void) or a distinguished value indicating that no decision has been made. Initially an interactive proof of the existence of such a procedure is given, for the fragment of type theory representing classical propositional calculus. That proof turns out to have a very simple structure, the construction of which can easily be automated. Therefore we describe a tactical operator reflect (T) which takes an arbitrary terminating search strategy T as its argument and produces a proof of the existence of a partial decision procedure, the extract term of which simulates the strategy T. Effectively, we compile a meta-level search strategy into an object level functional program. Once we have the object-level procedure, it can be used to avoid execution of the meta-level program altogether where knowledge of its existence is sufficient, or executed in place of the meta-level program.
Download:NO ONLINE COPY

[Search These Pages] [DAI Home Page] [Comment]