Delivery-Date: 
From: Tobias.Nipkow@informatik.tu-muenchen.de
To: boyer@CLI.COM
Cc: qed@mcs.anl.gov
In-Reply-To: <qed-owner@mcs.anl.gov>'s message of Fri, 23 Apr 1993 02:02:28 +0200 <9304230002.AA19396@axiom.CLI.COM>
Subject: Reflection?
Message-Id: <93Apr23.130937met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 23 Apr 1993 13:09:30 +0200
Sender: qed-owner@mcs.anl.gov
Precedence: bulk

Bob Boyer wrote:

> It wouldn't do one any good that I can see to prove the correctness of
> some algorithm in some random theory one layer removed because the
> right to reflect algorithms cannot in general be granted for just any
> logic represented in the root logic, as far as I can see.

There is a way out which has its own advantages and disadvantages. In order
to be able to refelct algorithms "in some random theory one layer removed"
you should

1. define the semantics of some programming language PL as another theory in
the system;
2. define a translation between your "random theory" and PL;
3. prove that evaluation in PL preserves equivalence in the logic.

Point 3 is very similar to the meta-functions approach in NQTHM. The
disadvantage is that you have to trust the semantics. But if the Root Logic
already contains a programming language you have the same problem. The
advantage is that you are not tied to one programming language.

Tobias