Norman Danner
Publications

Refereed publications

Circuit Principles and Weak Pigeonhole Variants (with C. Pollett)

To appear in Computing: The Australasian Theory Symposium (Newcastle, Australia, 2005). (PDF)

Abstract: This paper considers the relational versions of the surjective and multifunction weak pigeonhole principles for $\mathit{PV}$, $\Sigma^b_1$ and $\Theta^b_2$-formulas. We show that the relational surjective pigeonhole principle for $\Theta^b_2$ formulas in $S^1_2$ implies a circuit block-recognition principle which in turn implies the surjective weak pigeonhole principle for $\Sigma^b_1$ formulas. We introduce a class of predicates corresponding to poly-log length iterates of polynomial-time computable predicates and show that over $R^2_2$, the multifunction pigeonhole principle for such predicates is equivalent to an ``iterative'' circuit block-recognition principle. A consequence of this is that if $R^2_3$ proves this circuit iteration principle then RSA is vulnerable to quasi-polynomial time attacks.

Minimization and $\mathbf{NP}$ multifunctions (with C. Pollett)

Theoretical Computer Science 318(1-2):105-119, 2004. Note: Because Elsevier owns the copyright to this paper, I am not permitted to post a copy here.

Abstract: The implicit characterizations of the polynomial-time computable functions $\mathbf{FP}$ given by Bellantoni-Cook and Leivant suggest that this class is the complexity-theoretic analog of the primitive recursive functions. Hence it is natural to add minimization operators to these characterizations and investigate the resulting class of partial functions as a candidate for the analog of the partial recursive functions. We do so in this paper for Cobham's definition of $\mathbf{FP}$ by bounded recursion and for Bellantoni-Cook's safe recursion and prove that the resulting classes capture exactly $\mathbf{NPMV}$, the nondeterministic polynomial-time computable partial multifunctions. We also consider the relationship between our schemes and a notion of nondeterministic recursion defined by Leivant and show that the latter characterizes the total functions of $\mathbf{NPMV}$. We view these results as giving evidence that $\mathbf{NPMV}$ is the appropriate analog of partial recursive. This view is reinforced by earlier results of Spreen and Stahl who show that for many of the relationships between partial recursive functions and r.e. sets, analogous relationships hold between $\mathbf{NPMV}$ and $\mathbf{NP}$ sets. Furthermore, since $\mathbf{NPMV}$ is obtained from $\mathbf{FP}$ in the same way as the recursive functions are obtained from the primitive recursive functions (when defined via function schemes), this also gives further evidence that $\mathbf{FP}$ is properly seen as playing the role of primitive recursion.

Ramified recurrence with dependent types

In S. Abramsky (ed.), Typed $\lambda$-Calculi and Applications (Kraków 2001), pp. 91-105. Springer-Verlag (Lecture Notes in Computer Science 2044), Berlin, 2001. (PDF)

Abstract: We present a version of Gödel's system $T$ in which the types are ramified in the style of Leivant and a system of dependent typing is introduced. The dependent typing allows the definition of recursively defined types, where the recursion is controlled by ramification; these recursively defined types in turn allow the definition of functions by repeated iteration. We then analyze a subsystem of the full system and show that it defines exactly the primitive recursive functions. This result supports the view that when data use is regulated (for example, by ramification), standard function constructions are intimately connected with standard type-theoretic constructions.

Stratified polymorphism and primitive recursion (with D. Leivant)

Mathematical Structures in Computer Science 9(4):507-522, 1999. (PDF)

Abstract: Natural restrictions on the syntax of the second order (i.e. polymorphic) lambda calculus are of interest for programming language theory. In [1] one of the authors showed that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level $\mathcal E_4$ in the Grzegorczyk Hierarchy). We define here a second order lambda calculus in which type abstraction is stratified to levels up to $\omega^\omega$, an ordinal that permits highly uniform (and finite) type inference rules. Referring to this system, we show that the numeric functions definable in the calculus using ranks $< \omega^\ell$ are precisely Grzegorczyk's class $\mathcal E_{\ell+3}$ ($\ell \geq 1)$. This generalizes [1], where this is proved for $\ell = 1$. Thus, the numeric functions definable in our calculus are precisely the primitive recursive functions.

Ordinals and ordinal functions representable in the simply typed lambda-calculus

Annals of Pure and Applied Logic 97(1-3):179-201, 1999. Note: Because Elsevier owns the copyright to this paper, I am not permitted to post a copy here.

Abstract: We define ordinal representations in the simply typed lambda calculus, and consider the ordinal functions representable with respect to these notations. The results of this paper have the same flavor as those of Schwichtenberg and Statman on numeric functions representable in the simply typed lambda calculus. We define four families of ordinal notations; in order of increasing generality of the type of notation, the representable functions consist of the closure under composition of (1) successor and $\alpha\mapsto\omega\alpha$, (2) addition and $\alpha\mapsto\omega\alpha$, (3) addition and multiplication, and (4) addition, multiplication, and a ``weak'' discriminator.

On the foundations of corecursion (with L. Moss)

Logic Journal of the IGPL 5(2):231-257, 1997.

Abstract: We consider foundational questions related to the definition of functions by corecursion. This method is especially suited to functions into the greatest fixed point of some monotone operator, and it is most applicable in the context of non-wellfounded sets. We review the work on the Special Final Coalgebra Theorem of Aczel and the Corecursion Theorem of Barwise and Moss. We offer a condition weaker than Aczel's condition of uniformity on maps, and then we prove a result relating the operators satisfying the new condition to the smooth operators of Barwise and Moss.

Toward a model theory of diagrams (with E. Hammer)

Journal of Philosophical Logic 25(5), 1996.

Other publications

Book review of Derivation and Computation: Taking the Curry-Howard Correspondence Seriously (by H. Simmons)

Bulletin of Symbolic Logic 7(3):380-383, 2001.

Ordinal Notations in Typed $\lambda$-Calculi

Ph.D. dissertation, Indiana University, 1999.

Abstract: In this thesis, we investigate the use of various typed $\lambda$-calculi as a basis for ordinal notations. Traditionally, an ordinal notation is constructed as a numeric code, an approach that obscures intuitive notions of complexity. By extending the Church numerals of the $\lambda$-calculus to transfinite ordinal notations, we are able to meet two complexity-theoretic criteria: (1) passing to a limit in the construction of an ordinal (the ``complex'' step) is made explicit, and (2) there are natural syntactic requirements that restrict the complexity of the possible notations (and hence the ordinals for which there are notations). We carry out this program for the simply typed $\lambda$-calculus and the transfinitely ramified polymorphic $\lambda$-calculus. For the simply typed calculus, we introduce several classes of notations and characterize both the ordinals and ordinal functions representable with respect to each class. For the ramified $\lambda$-calculus, we calibrate the representable ordinals against the degree of ramification. We also define environment model semantics for transfinitely ramified polymorphism and prove that the semantics is sound and complete for $\beta\eta$-conversion, and investigate iteration functionals in the type structure over the ordinals.

Bibliography

1

D. Leivant.
Finitely stratified polymorphism.
Information and Computation, 93(1):93-113, 1991.

About this document ...

Norman Danner
Publications

This document was generated using the LaTeX2HTML translator Version 2002 (1.62)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 papers

The translation was initiated by Norman Danner on 2004-11-05