Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 11 May 94 16:43:48 EDT
From: reetz <reetz@ira.uka.de>
To: reetz@ira.uka.de, info-hol@leopard.cs.byu.edu
Subject: RE: does there exists a hol-lex?
Message-Id: <"i80fs2.ira.217:11.04.94.14.43.51"@ira.uka.de>

Konrad writes:

    A. Write your own parser for all HOL terms, including your new
       language.
 
    B. Write a parser for your new language, and somehow insert its
       results into HOL terms.

Well, I don't want to use A., because what if HOL90.whateverversion
changes its syntax, again? I'm afraid my own stuff won't be
compatible. So, what about B in detail? Embedding an own language,
one has to formally embed typechecking, too. So one can even
reason about typechecking... So, polymorphy won't be a problem.
I didn't understand what Konrad wrote about antiquotation.
Can somebody give me further details? My idea was to represent
sentences of the new language as a string in hol and define
a parser as a hol constant, which maps strings into the semantics
of the new language (or into an error, if e.g. typechecking fails).

What is the advantage of this? Terms are better to read and you
can ``attack'' those ``nice'' properties of some languages where
you can define subtypes of numbers and members of these
different types aren't compatible, meaning you might end up
with something like |- ~(5:num1) = (5:num2). Or putting it
more abstract: sometimes you don't want to mix the types
of your new language with the hol-types.

IMHO, in my point of view, most(?) people have formalised languages
in HOL completly by hand. For small languages, that's just fine.
But what about some sort of ``baroque'' languages? You get stuck in
doing everything by hand. However, looking at compiler building,
we might like to get tools, which are formalised within
the logic (see typechecking above), which completly automate some stuff
like syntax and which produces better-to-read results.

Ralf

(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                            SFB 358 of the german research     *)
(*  reetz@informatik.uni-karlsruhe.de     society (DFG)                      *)
(*  reetz@ira.uka.de                      University of Karlsruhe, Germany   *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)