[Prev][Next][Index]
Tactics in LP?
-
To: Larch interest mailing list <larch-interest>
-
Subject: Tactics in LP?
-
From: Karl-Heinz Buth <khb@informatik.uni-kiel.dbp.de>
-
Date: Mon, 15 Feb 1993 18:19:03 +0100
-
X400-Content-Type: P2-1984 (2)
-
X400-Mts-Identifier: [/PRMD=uni-kiel/ADMD=dbp/C=de/;gutemine 017841.0729796743000]
-
X400-Originator: khb@informatik.uni-kiel.dbp.de
-
X400-Received: by mta ixgate.gmd.de in /PRMD=GmD/ADMD=DbP/C=DE/; Relayed; Tue, 16 Feb 1993 08:17:28 +0100
-
X400-Received: by /PRMD=uni-kiel/ADMD=dbp/C=de/; Relayed; Mon, 15 Feb 1993 18:19:03 +0100
-
X400-Recipients: larch-interest@src.dec.com
When working with LP in compiler verification, I have several times
seen the case that a proof consists of several subproofs that differ
only very little, if at all. This is because these proofs are done by
structural induction, and many of the cases are very similar. Now the
rewriting systems I use for these proofs are either very large or
non-confluent or contain non-terminating rules or a combination of all
of these, so I usually need a special strategy to control the
rewriting process.
This can be done by using an editor's copy/paste function, but it
would be much nicer if I could describe this strategy in a concise
way, like "first use rules A once, then normalize with rules B, then
use induction on x and then stop". Systems like HOL include the
feature that the user can define tactics for exactly this purpose. I
wouldn't say that one needs a whole programming language like ML on
top of LP, but something like
rewrite <names> with <names> using <tactic>
would already be a great help. Are there any plans to include such a
feature in future version of LP?
--
Karl-Heinz Buth
----------------------------------------------------------------
| Institut fuer Informatik, Universitaet Kiel, Germany |
| khb@informatik.uni-kiel.dbp.de Tel.: ++49-431-560421 |