[Prev][Next][Index][Thread]
papers available
Two papers "Fixpoint Technique for Counting Terms in Typed Lambda
Calculus" and "Lambda definability is decidable for second order
types and for regular third order types" are available by anonymous
ftp.
"Fixpoint Technique for Counting Terms in Typed Lambda Calculus"
Abstract: Typed lambda 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 and Roger
Hindlay. Similarly Hirokawa proved that complexity of the question whether
given type ( formula ) possess an infinite number of normal terms (proofs)
is polynomial space complete.
"Lambda definability is decidable for second order types and
for regular third order types"
Abstract: It has been proved by Loader that Statman-Plotkin conjecture
fails. It means that it is undecidable to determine whether or not the
given function in the full type hierarchy is lambda definable. The Loader
proof was done by encoding the word problem in the full type hierarchy
based on the domain with 7 elements. The aim of this paper is to show that
the lambda definability problem limited for second order types and regular
third order types is decidable in any finite domain. Obviously lambda
definability is decidable for 0 and 1 order types. As an additional effect
of the result described we may observe that for certain types there is no
finite grammar generating all closed terms.
For anonymous ftp, connect to: ftp.cs.buffalo.edu
and copy the file: pub/tech-reports/95-20.ps.Z
or: pub/tech-reports/95-24.ps.Z
using binary mode transfer.
With best regards,
Marek Zaionc