Abstract
This talk answers the open problem of finding a type system that
characterizes hereditary permutators. First this talk shows that
there does not exist such a type system by showing that the set of
hereditary permutators is not recursively enumerable. The set of
positive primitive recursive functions is used to prove it. Secondly
this talk gives a best-possible solution by providing a countably
infinite set of types such that a term has every type in the set if
and only if the term is a hereditary permutator. By the same
technique for the first claim, this talk also shows that a set of
normalizing terms in infinite lambda-calculus is not recursively
enumerable if it contains some term having a computable infinite path,
and shows the set of streams is not recursively enumerable.
This work was presented at LICS 2008.
Short bio
2001--present Professor, National Institute of Informatics
1996--2001 Associate Professor, University of Tokyo
1994--1996 Associate Professor, Tohoku University
1989--1994 Research Associate, Tohoku University
1993 Ph.D in Science, University of Tokyo
1987 Master's in Science, University of Tokyo
1985 Bachelor n Science, University of Tokyo
1983 Bachelor in Law, University of Tokyo
Resources
This will be shown to users with no Flash or Javascript.
|
