Author name cluster

J.W. Klop

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.

9 papers

1 author row

TCS Journal 1997 Journal Article

Infinitary lambda calculus

J.R. Kennaway
J.W. Klop
M.R. Sleep
F.J. de Vries

In a previous paper we have established the theory of transfinite reduction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. From the viewpoint of infinitary rewriting, the Böhm model of the lambda calculus can be seen as an infinitary term model. In contrast to term rewriting, there are several different possible notions of infinite term, which give rise to different Böhm-like models, which embody different notions of lazy or eager computation.

Details DOI

I&C Journal 1995 Journal Article

Transfinite Reductions in Orthogonal Term Rewriting Systems

R. Kennaway
J.W. Klop
R. Sleep
F.J. Devries

We define the notion of transfinite term rewriting: rewriting in which terms may be infinitely large and rewrite sequences may be of any ordinal length. For orthogonal rewrite systems, some fundamental properties known in the finite case are extended to the transfinite case. Among these are the Parallel Moves lemma and the Unique Normal Form property. The transfinite Church-Rosser property (CR∞) fails in general, even for orthogonal systems, including such well-known systems as combinatory logic. Syntactic characterisations are given of some classes of orthogonal TRSs which do satisfy CR∞. We also prove a weakening of CR∞ for all orthogonal systems, in which the property is only required to hold up to a certain equivalence relation on terms. Finally, we extend the theory of needed reduction from the finite to the transfinite case. The reduction strategy of needed reduction is normalising in the finite case, but not in the transfinite case. To obtain a normalising strategy, it is necessary and sufficient to add a requirement of fairness. Parallel outermost reduction is such a strategy.

Details DOI

TCS Journal 1989 Journal Article

Term-rewriting systems with rule priorities

J.C.M. Baeten
J.A. Bergstra
J.W. Klop
W.P. Weijland

In this paper we discuss term-rewriting systems with rule priorities, which simply is a partial ordering on the rules. The procedural meaning of such an ordering then is, that the application of a rule of lower priority is allowed only if no rule of higher priority is applicable. The semantics of such a system is discussed. It turns out that the class of all bounded systems indeed has such a semantics.

Details DOI

I&C Journal 1989 Journal Article

Unique normal forms for lambda calculus with surjective pairing

J.W. Klop
R.C. de Vrijer

We consider the equational theory λπ of λ-calculus extended with constants π, π 0, π 1 and axioms for surjective pairing: π 0(πXY) = X, π 1(πXY) = Y, π(π 0 X)(π 1 X) = X. Two reduction systems yielding the equality of λπ are introduced; the first is not confluent and, for the second, confluence is an open problem. It is shown, however, that in both systems each term possessing a normal form has a unique normal form. Some additional properties and problems in the syntactical analysis of λπ and the corresponding reduction systems are discussed.

Details DOI

I&C Journal 1987 Journal Article

Needed reduction and spine strategies for the lambda calculus

H.P. Barendregt
J.R. Kennaway
J.W. Klop
M.R. Sleep

A redex R in a lambda-term M is called needed if in every reduction of M to normal form (some residual of) R is contracted. Among others the following results are proved: 1. R is needed in M iff R is contracted in the leftmost reduction path of M. 2. Let R: M 0 →M 1 → M 2 → … reduce redexes R i: M i → M i+1, and have the property that ∀i. ∃j≥i. R j is needed in M j. Then R is normalising, i. e. , if M 0 has a normal form, then R is finite and terminates at that normal form. 3. Neededness is an undecidable property, but has several efficiently decidable approximations, various versions of the so-called spine redexes.

Details DOI

TCS Journal 1987 Journal Article

On the consistency of Koomen's Fair Abstraction Rule

J.C.M. Baeten
J.A. Bergstra
J.W. Klop

We construct a graph model for ACPτ, the algebra of communicating processes with silent steps, in which Koomen's Fair Abstraction Rule (KFAR) holds, and also versions of the Approximation Induction Principle (AIP) and the Recursive Definition & Specification Principles (RDP&RSP). We use this model to prove that in ACPT (but not in ACP!) each computably recursively definable process is finitely recursively definable.

Details DOI

TCS Journal 1985 Journal Article

Algebra of communicating processes with abstraction

J.A. Bergstra
J.W. Klop

We present an axiom system ACP, for communicating processes with silent actions (‘τ-steps’). The system is an extension of ACP, Algebra of Communicating Processes, with Milner's τ-laws and an explicit abstraction operator. By means of a model of finite acyclic process graphs for ACPτ, syntactic properties such as consistency and conservativity over ACP are proved. Furthermore, the Expansion Theorem for ACP is shown to carry over to ACPτ. Finally, termination of rewriting terms according to the ACPτ, axioms is probed using the method of recursive path orderings.

Details DOI

TCS Journal 1984 Journal Article

Linear time and branching time semantics for recursion with merge

J.W. de Bakker
J.A. Bergstra
J.W. Klop
J.-J.Ch. Meyer

We consider two ways of assigning semantics to a class of statements built from a set of atomic actions (the ‘alphabet’), by means of sequential composition, nondeterministic choice, recursion and merge (arbitrary interleaving). The first is linear time semantics (LT), stated in terms of trace theory; the semantic domain is the collection of all closed sets of finite and infinite words. The second is branching time semantics (BT), as introduced by De Bakker and Zucker; here the semantic domain is the metric completion of the collection of finite processes. For LT we prove the continuity of the operations (merge, sequential composition) in a direct, combinatorial way. Next, a connection between LT and BT is established by means of the operation trace which assigns to a process its set of traces. We show that the trace set of a process is closed and that trace is continuous. This requires the compactness of the semantic domains, ensured by the finiteness of the alphabet. Using trace, we then can carry over BT into LT.

Details DOI

TCS Journal 1984 Journal Article

Proving program inclusion using Hoare's logic

J.A. Bergstra
J.W. Klop

We explore conservative refinements of specifications. These form a quite appropriate framework for a proof theory for program inclusion based on a proof theory for program correctness. We propose two formalized proof methods for program inclusion and prove these to be sound. Both methods are incomplete but seem to cover most natural cases.

Details DOI