Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05252-0@swan.cl.cam.ac.uk>; Fri, 15 May 1992 10:44:27 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02947; Fri, 15 May 92 02:32:38 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA02943; Fri, 15 May 92 02:32:30 -0700 Received: by grolsch.cs.ubc.ca id AA28622 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Fri, 15 May 1992 02:32:56 -0700 Date: 15 May 92 2:32 -0700 From: Sreeranga Rajan To: etxhsan@se.ericsson.brazil Cc: info-hol@edu.uidaho.cs.ted Message-Id: <367*sree@cs.ubc.ca> Subject: Re: Ackermann's function I don't think HOL's type system (based on Church's simple theory of types) as it is, is not expressive enough to derive Girard's result. You would need System T (or better Girard's System F) to have recursion on complex types (such as int -> int). Regards, -Sree (sree@cs.ubc.ca)