Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: John.Harrison@cl.cam.ac.uk
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:105240:940526202303"@cl.cam.ac.uk> (message from John Harrison on Thu, 26 May 1994 22:22:50 +0200)
Subject: Re: What's up for grabs?
Message-Id: <94May26.232320met_dst.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 26 May 1994 23:23:16 +0200


John Harrison writes:

> So might one take set theory as basic and use type theory as an
> organizational tool built on top of that (or not at all)?

This leads to another question: what are the essential differences
between HOL and set theory?

Things that spring to mind in favour of HOL:

    - type constructors in HOL give an abbreviation facility that can be
      extremely important in shrinking the size of expressions. This is
      good from the point of view of the user (small expressions are
      easier to grasp, especially with type information suppressed), and
      from the view of the logic implementor (small expressions help the
      system run faster). 

    - functions are intensional (and easily made extensional) and there
      is a built-in reduction mechanism (BETA_CONV) that isn't available
      in set theory.

Konrad.