Just Say No!

The Transformational Approach to Negation in a Logical Framework

Alberto Momigliano June 30, 2000

Department of Philosophy Carnegie Mellon University Pittsburgh, PA 15213

Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy

Thesis Committee: Frank Pfenning, Chair Dana Scott Dale Miller, Pennsylvania State University

Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000 Alberto Momigliano

Abstract

We address the issue of endowing a logical framework with a logically justified notion of negation. Logical frameworks with a logic programming interpretation such as hereditary Harrop formulae cannot directly express negative information, although negation is a useful specification tool. Since negation-as-failure does not fit well in a logical framework, especially one endowed with hypothetical and parametric judgments, we adapt the idea of elimination of negation from Horn logic to a fragment of higher-order hereditary Harrop formulae. The idea is to replace occurrences of negative predicates with positive ones which are operationally equivalent. This entails two separate phases.

Complementing terms, i.e in our case higher-order patterns. Due the presence of partially applied lambda terms, intuitionistic lambda calculi are not closed under complementation. We thus develop a strict lambda calculus, where we can directly express whether a function depends on its argument.

Complementing clauses. This can be seen as a negation normal form procedure which is consistent with intuitionistic provability. It entails finding a middle ground between the Closed World Assumption usually associated with negation and the Open World Assumption typical of logical frameworks. As this is in general not possible, we restrict ourselves to a fragment in which clause complementation is viable and that has proven to be expressive enough for the practice of logical frameworks. The main technical idea is to isolate a set of programs where static and dynamic clauses do not overlap.

Acknowledgments

This dissertation would not have been possible without the help and support of many different people. First and foremost my thesis advisor, Frank Pfenning, who has guided me through every element of this reseat, from the high level design decisions down to the most technical details. In the process, he has taught me a rigorous discipline and style in approaching formal problems that has made me a far better researcher.

I am also deeply grateful to Carsten Schürmann, who, under the motto ”What do you want to prove today?” has always been ready and willing to share his considerable knowledge from type-theory to the practicalities of the Twelf system. I’m also indebted to Roberto Virga for many discussions and his precious help in debugging the strict calculus rules.

In the health department, I want to thanks from the deep of my heart Dr. Garfinkel, Dr. Velletri, Dr Oliva, Dr. Zigler, last but not least Jean Bender and the wonderful people at GAV.

I wouldn’t have been able to survive all those years in Pittsburgh without the company of the local Italian community and friends: Barbara and Jerry, Cristina and Massimo, Cristina and Dude, Ulrike and Massimo, Stefano and Kathy, Giovanna and Aldo. A particular thanks to Lena.

Finally, I want to thank my beloved Claudia, who has been waiting for me on the other part of the ocean, so very patient and affectionate during those hard and long years of separation.

It is so sad that my mother is not here anymore to witness the happy conclusion of such a difficult journey. All I can do is dedicate this dissertation to her memory.

2

\underline{i}

Draft of June 30, 2000

\underline{ii}

Draft of June 30, 2000

Contents

iii

iv  CONTENTS

List of Figures

v

vi  LIST OF FIGURES