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: des@inmos.co.uk
Cc: Richard.Boulton@cl.cam.ac.uk, hol2000@leopard.cs.byu.edu
In-Reply-To: <24175.9405251145@frogland.inmos.co.uk> (message from David Shepherd on Wed, 25 May 1994 13:45:24 +0200)
Subject: Re: Basic changes: lambda abstraction
Message-Id: <94May25.141348met_dst.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 25 May 1994 14:13:43 +0200


Richard Boulton writes:

> Having said that, there is a strong case for making abstractions over tuples
> built-in. In fact, is there any reason why such a construct can't subsume the
> existing ABS, it being taken as the special case in which the tuple has one
> component?

Maybe we should go further and provide for ML-style patterns in HOL
lambda abstractions. The problem is what to do with unmatched patterns:
for instance one could define predecessor as

    \(SUC x). x

but what would beta-conversion do if this was applied to `0`? In ML the
runtime system can raise a Match exception, but there isn't an analogue
to exception in a logic of total functions, as far as I know.

One could go further yet and provide abstraction over less restricted
syntactic forms, e.g. the set of terms equivalent to an ML-style pattern
(example: `\(K x y). 2*x`) but that seems kind of wacky.

Konrad.