Author name cluster

Daniel J. Dougherty

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

TCS Journal 2008 Journal Article

Characterizing strong normalization in the Curien–Herbelin symmetric lambda calculus: Extending the Coppo–Dezani heritage

Daniel J. Dougherty
Silvia Ghilezan
Pierre Lescanne

We develop an intersection type system for the λ ¯ μ μ ˜ calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for λ ¯ μ μ ˜: in addition to characterizing the λ ¯ μ μ ˜ expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.

Details DOI

TCS Journal 2006 Journal Article

Normal forms for binary relations

Daniel J. Dougherty
Claudio Gutiérrez

We consider the representable equational theory of binary relations, in a language expressing composition, converse, and lattice operations. By working directly with a presentation of relation expressions as graphs we are able to define a notion of reduction which is confluent and strongly normalizing and induces a notion of computable normal form for terms. This notion of reduction thus leads to a computational interpretation of the representable theory.

Details DOI

LPAR Conference 2005 Conference Paper

Strong Normalization of the Dual Classical Sequent Calculus

Daniel J. Dougherty
Silvia Ghilezan
Pierre Lescanne
Silvia Likavec

Abstract We investigate some syntactic properties of Wadler’s dual calculus, a term calculus which corresponds to classical sequent logic in the same way that Parigot’s λμ calculus corresponds to classical natural deduction. Our main result is strong normalization theorem for reduction in the dual calculus; we also prove some confluence results for the typed and untyped versions of the system.

Details

I&C Journal 2000 Journal Article

Equality between Functionals in the Presence of Coproducts

Daniel J. Dougherty
Ramesh Subrahmanyam

We consider the lambda calculus obtained from the simply typed calculus by adding products, coproducts, and a terminal type. We prove the following theorem: The equations provable in this calculus are precisely those true in any set-theoretic model with an infinite base type.

Details DOI

TCS Journal 1998 Journal Article

Equational unification, word unification, and 2nd-order equational unification

Friedrich Otto
Paliath Narendran
Daniel J. Dougherty

For finite convergent term-rewriting systems it is shown that the equational unification problem is recursively independent of the equational matching problem, the word matching problem, and the 2nd-order equational matching problem. Apart from the latter these results are derived by considering term-rewriting systems on signatures that contain unary function symbols only (i. e. , string-rewriting systems). Also for this special case 2nd-order equational matching is shown to be reducible to 1st-order equational matching. In addition, we present some new decidability results for simultaneous equational matching and unification. Finally, we compare the word unification problem to the 2nd-order equational unification problem.

Details DOI

TCS Journal 1995 Journal Article

A combinatory logic approach to higher-order E-unification

Daniel J. Dougherty
Patricia Johann

Let E be a first-order equational theory. A translation of higher-order E-unification problems into a combinatory logic framework is presented and justified. The case in which E admits presentation as a convergent term rewriting system is treated in detail: in this situation, a modification of ordinary narrowing is shown to be a complete method for enumerating higher-order E-unifiers. In fact, we treat a more general problem, in which the types of terms contain type variables.

Details DOI

TCS Journal 1993 Journal Article

Higher-order unification via combinators

Daniel J. Dougherty

We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type variables, so that a solution may involve type-substitution as well as term substitution. The problem is first translated into the problem of unification with respect to exstensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms.

Details DOI

I&C Journal 1992 Journal Article

Adding algebraic rewriting to the untyped lambda calculus

Daniel J. Dougherty

We investigate the system obtained by adding an algebraic rewriting system R to an untyped lambda calculus in which terms are formed using the function symbols from R as constants. On certain classes of terms, called here “stable, ” we prove that the resulting calculus is confluent if R is confluent, and is terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result suggests a general method for proving confluence of typed β-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.

Details DOI