Return-Path: <kfoury@cs.bu.edu> Received: from cs.bu.edu (cs [128.197.12.2]) by cs3.bu.edu (8.12.11/8.12.11) with ESMTP id i91NYcuh032169; Fri, 1 Oct 2004 19:34:38 -0400 Received: from cs.bu.edu (h000c41248e2b.ne.client2.attbi.com [24.34.20.189]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i91NYc9N012727 for <cs520@cs.bu.edu>; Fri, 1 Oct 2004 19:34:38 -0400 (EDT) Message-ID: <415DE992.9080401@cs.bu.edu> Date: Fri, 01 Oct 2004 19:34:42 -0400 From: Assaf Kfoury <kfoury@cs.bu.edu> Organization: Boston University User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.6) Gecko/20040413 Debian/1.6-5 X-Accept-Language: en To: cs520 Course Account <cs520@cs.bu.edu> Subject: hint for problem 2 in problem set 3 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Spam-HitLevel: xx X-Spam-DCC: SPAMCHECK.NET: cs3.bu.edu 1168; Body=19 Fuz1=19 Fuz2=19 X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on cs3.bu.edu X-Spam-Level: ** X-Spam-Status: No, hits=2.4 required=10.0 tests=AWL,RCVD_IN_DSBL, RCVD_IN_NJABL_PROXY autolearn=no version=2.64 X-Spam-Pyzor: Reported 0 times. Status: RO X-Mozilla-Status: 8001 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000e8c
Of the 5 parts mentioned in Problem 2, only part 5 requires some
non-trivial work. The first 4 parts explains how to show that ((a -> b)
-> a) -> a is not a tautology of implicational logic, provided part 5 is
true.
As pointed out in part 3, you can assume that strong normalization holds
for the evaluation of simply-typed terms according to full beta-reduction.
For part 5, you need to consider the "shapes" of simply-typed terms that
are (1) closed and (2) in normal form according to full beta-reduction.
By the "shape" of a term I mean its parse tree. Suppose you have a term
t satisfying (1) and (2). First argue that the root node (of the parse
tree of t) cannot be an application node. Then argue that the root node
must be a lambda binding. Then argue that the scope of this outermost
lambda binding cannot be a lambda binding nor a variable, and therefore
must be an application -- if we hope to show that ((a -> b) -> a) -> a
is a possible type for it. And then continue in the same way in order to
show there is no term satisfying both (1) and (2) which has type ((a ->
b) -> a) -> a ...
Assaf
This archive was generated by hypermail 2b29 : Fri Nov 19 2004 - 17:00:43 EST