Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: Konrad Slind <slind@informatik.tu-muenchen.de>
Cc: john.harrison@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: Difficulties with large terms
In-Reply-To: Your message of "Thu, 26 Jan 1995 15:03:58 +0100." <95Jan26.150403met.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 26 Jan 1995 18:24:46 +0000
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:124940:950126184535"@cl.cam.ac.uk>


> 1. HOL doesn't have a particularly efficient implementation of the
>    lambda calculus. I don't think anybody else does either - it's a
>    major problem to have optimal implementations of substitution, aconv,
>    computation of free variables, computation of types, and
>    con-and-de-struction of terms. 

There's an interesting issue surrounding this question.  I believe
that the most "efficient implementation of the lambda calculus" may
well end up depending very much on the intended application. Suppose,
for example, you can have only one of

  1) fast aconv, slow substitution
  2) slow aconv, fast substitution

In a (classical, HOL-like) theorem prover it's on the whole preferable
to be in situation (1), since almost every inference involves checking
alpha-equivalence.  But in a functional programming language, where
doing reductions is the game, situation (2) is better.  Opinions as to
what's a good term representation depend on whether you're a functional
programmer or a theorem proving engineer.

Of course, we'd like to have

  3) fast aconv, fast substitution

but then maybe this would break something else.  So pending the perfect
representation, one needs to weigh up the alternatives in an application
specific context.

Tom