Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <20673-0@swan.cl.cam.ac.uk>; Sun, 12 Jan 1992 12:40:23 +0000
Received: by ted.cs.uidaho.edu.cs.uidaho.edu (16.6/1.34) id AA20360;
          Sun, 12 Jan 92 04:30:48 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Sunset.AI.SRI.COM by ted.cs.uidaho.edu.cs.uidaho.edu (16.6/1.34)
          id AA20356; Sun, 12 Jan 92 04:30:44 -0800
Received: from cam.sri.com by Sunset.AI.SRI.COM (4.1/SMI-4.1) id AA21088
          for info-hol@ted.cs.uidaho.edu; Sun, 12 Jan 92 04:33:08 PST
Received: from harlech.cam.sri.com by cam.sri.com (4.1/4.16) id AA20129
          for murthy@margaux.inria.fr; Sun, 12 Jan 92 12:32:54 GMT
Received: by harlech.cam.sri.com (4.1/4.16) id AA10003
          for info-hol@ted.cs.uidaho.edu; Sun, 12 Jan 92 12:32:51 GMT
Date: Sun, 12 Jan 92 12:32:51 GMT
From: Mike Gordon <mjcg%cam.sri.com@com.sri.ai>
Message-Id: <9201121232.AA10003@harlech.cam.sri.com>
To: murthy@fr.inria.margaux
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: murthy@margaux.inria.fr's message of Sun, 12 Jan 92 02:37:12 N <9201120137.AA05187@margaux.inria.fr>
Subject: Bound Variables



   >How are bound variables represented in terms in HOL?  I mean, in the
   >actual, physical representation of lambda(x.b), are occurrences of "x"
   >in "b" a string, or a number?


Hi,

In Classic HOL (HOL88) occurrences of `x` are used, not De Bruijn
indices. For example, the term "\x. x+1" is represented internally by
the S-expression:

(abs ((var x num)
      comb
      ((comb ((const + fun (num) (fun (num) (num))) var x num) fun (num) (num))
       const
       |1|
       num)
      num)
     fun
     (num)
     (num))

Note that there is some structure sharing which is not visible in this
pretty-printing.

I'm not sure how bound variables are represented in HOL90 or ICL-HOL.
Maybe their implementers will reply to your message.

Mike