page 1  (13 pages)
2to next section

FIXPOINT TECHNIQUE FOR COUNTING

TERMS IN TYPED >= CALCULUS 1

Marek Zaionc 2

email: zaionc@cs.buffalo.edu

Abstract: Typed >= calculus with denumerable set of ground types is considered. The aim of the paper is to show procedure for counting closed terms in long normal forms. It is shown that there is a surprising correspondence between the number of closed terms and the fixpoint solution of the polynomial equation in some complete lattice. It is proved that counting of terms in typed lambda calculus can be reduced to the problem of finding least fixpoint for the system of polynomial equations. The algorithm for finding the least fixpoint of the system of polynomials is considered. By the well known Curry Howard isomorphism the result can be interpreted as a method for counting proofs in the implicational fragment of the propositional intuitionistic logic. The problem of number of terms was studied but never published by Ben- Yelles (see [3] ). Similarly in [4] it was proved that complexity of the question whether given type possess an infinite number of normal terms is polynomial space complete.

1. Typed >= calculus.

The set TY PES is defined as follows: there is a denumerable set of ground types fA; B; :::g and if o and ? are types then o ! ? is a type. We will use the following notation: if ?; o1; :::; on are types then by ?nj=1oj ! ? we mean the type o1 ! (:::(on ! ?):::). Therefore, every type o has the form ?nj=1oj ! ? where ? is a ground type. If o is a type of the form ?nj=1oj ! ? where ? is a ground type, then oi for i <= n are called components of type o and are denoted by o [i].

For any type o we define rank(o) and arg(o) as follows: arg(o) = rank(o) = for every ground type o and arg(?nj=1o [j] ! ?) = n and rank(?nj=1o [j] ! ?) = maxi=1:::n rank(o [i]) + 1. We define inductively types o [i1; :::; ik] by (o [i1; :::; ik?1])[ik] for 1 <= ik <= arg(o [i1 ; :::; ik?1]). Ground types o and ? are equivalent (denoted by o ? ?) if o = ?. This relation is extended to all types by the following rules: (o ! ?) ? ? iff ? ? ? and o ? (? ! ?) iff o ? ?.
For any type o there is given a denumerable set of variables V (o ). Any variable of type o is a term of type o . If T is a term of type o ! ? and S is a term of type o , then TS is a term of type ?. If T is a term of type ? and x is a variable of type o , then >=x:T is a term of type o ! ?. The axioms of equality between terms have the form of ? conversions and the convertible terms will be written as T = ? S. Term T is in long normal form if T = >=x1:::xn:yT1:::Tk where y is an xi for some i <= n or y is a free variable, Tj for j <= k are in the long normal form and yT1...Tk is a term of some ground type. For a closed term T = >=x1:::xn:xiT1:::Tk variable xi is called a heading. Long normal forms exist and are unique for ? conversions (compare [6]).

1Supported by KBN research grant 0384/P4/93
2Permanent address of the author is: Computer Science Department, Jagiellonian University Nawojki 11, 30-072 Krakow, Poland E-mail zaionc@ii.uj.edu.pl. This paper was partially prepared while author was visiting Computer Science Department at State University of New York at Buffalo, USA