Delivery-Date: 
To: qed@mcs.anl.gov
cc: info-hol@leopard.cs.byu.edu
Subject: Paper on reflection
Date: Mon, 24 Apr 1995 21:21:24 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:122480:950424202132"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


In view of the lively discussion of reflection principles at the last QED
workshop, readers of this mailing list may be interested in the following:

  Metatheory and Reflection in Theorem Proving: A Survey and Critique
  John Harrison
  SRI Technical Report CRC-053

It's a bit long and discursive. A shorter and more incisive version may appear
eventually, but in the meantime I welcome any comments from dogged readers.

It can be obtained electronically via the Web at "http://www.cam.sri.com", or
by FTP from "ftp.cl.cam.ac.uk" as "hvg/papers/Reflection.*". Abstract:

  One way to ensure correctness of the inference performed by computer
  theorem provers is to force all proofs to be done step by step in a simple,
  more or less traditional, deductive system. Using techniques pioneered in
  Edinburgh LCF, this can be made palatable. However, some believe such an
  approach will never be efficient enough for large, complex proofs. One
  alternative, commonly called `reflection', is to analyze proofs using a
  second layer of logic, a `metalogic', and so justify abbreviating or
  simplifying proofs, making the kinds of shortcuts humans often do or
  appealing to specialized decision algorithms. In this paper we contrast the
  fully-expansive LCF approach with the use of reflection. We put forward
  arguments to suggest that the inadequacy of the LCF approach has not been
  adequately demonstrated, and neither has the practical utility of
  reflection (notwithstanding its undoubted intellectual interest). The LCF
  system with which we are most concerned is the HOL proof assistant.

  The plan of the paper is as follows. We examine ways of providing user
  extensibility for theorem provers, which naturally places the LCF and
  reflective approaches in opposition. A detailed introduction to LCF is
  provided, emphasizing ways in which it can be made efficient. Next, we
  present a short introduction to metatheory and its usefulness, and,
  starting from G\"odel's proofs and Feferman's transfinite progressions
  of theories, look at logical `reflection principles'. We show how to
  introduce computational `reflection principles' which do not extend the
  power of the logic, but may make deductions in it more efficient, and
  speculate about their practical usefulness. Applications or proposed
  applications of computational reflection in theorem proving are
  surveyed, following which we draw some conclusions. In an appendix, we
  attempt to clarify a couple of other notions of `reflection' often
  encountered in the literature.

  The paper questions the too-easy acceptance of reflection principles as
  a practical necessity. However I hope it also serves as an adequate
  introduction to the concepts involved in reflection and a survey of
  relevant work. To this end, a rather extensive bibliography is provided.

John.