Delivery-Date: 
Date: Tue, 25 Apr 1995 06:26:22 GMT
From: rbj@campion.demon.co.uk (Roger Bishop Jones)
Message-Id: <3765@campion.demon.co.uk>
To: John.Harrison@cl.cam.ac.uk
Cc: qed@mcs.anl.gov
Subject: Re: Paper on reflection
Lines: 35
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

In message <"swan.cl.cam.:122480:950424202132"@cl.cam.ac.uk> John Harrison writes:
> 
> 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.

Taking you at your word I offer the following observations on your abstract:

<snip>

>   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.

I don't see why a reflection principle should be regarded as "in opposition"
to the LCF paradigm.  The LCF paradigm can be applied to any logic however
complex its rules.  A reflection principle can be put into a logic and
implemented as a rule, using the LCF paradigm, in complete consistency with
anything that I would regard as essential to that paradigm.

I'm not suggesting that your primary concern isn't a real one, which is
about whether doing this would be worthwhile.  Just quibbling with your
description of the issue.

I would be interested to hear what the qed community considers to be
the definitive characteristic(s) of the LCF paradigm.

Roger Jones    http://www.to.icl.fi/ICLE/rbjpub/rbj.htm
at home        rbj@campion.demon.co.uk