Foster et al. proposed a linguistic approach to the bidirectional transformation, with lens. A lens is a pair of two functions, one is a forward transformation called get which produces a target view from an original source, and the other is a backward transformation called put which updates the original source to a new one with an updated view. The get and put functions depend on each other to be consistent. A lens is called well-behaved if it satisfies two lens laws, GetPut and PutGet. Every put function uniquely determines a get function if it exists, as far as the get and put functions form a well-behaved lens. Fischer et al. found the conditions of a put function under which the corresponding get function exists, where both get and put functions are supposed to be total. In this paper, we consider the case where get and put functions are possibly partial. We show that almost the same conditions as the ones given by Fischer et al. work well when only a put function is possibly partial, while they do not work when a get function is also possibly partial. In order to have similar results, we propose a new lens law for the case where both get and put functions are possibly partial.

A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. Proof methods for sufficient completeness of terminating TRSs have been well studied. In this paper, we introduce a simple derivation system for proving sufficient completeness of possibly non-terminating TRSs. The derivation system consists of rules to manipulate a set of guarded terms, and sufficient completeness of a TRS holds if there exists a successful derivation for each function symbol. We also show that variations of the derivation system are useful for proving special cases of local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness.

We present a framework for proving inductive theorems of first-order equational theories, using techniques of implicit induction developed in the field of term rewriting. In this framework, we make use of automated confluence provers, which have recently been developed intensively, as well as a novel condition of sufficient completeness, called local sufficient completeness. The condition is a key to automated proof of inductive theorems of term rewriting systems that include non-terminating functions. We also apply the technique to showing the correctness of program transformation that is realised as an equivalence transformation of term rewriting systems.

Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004; Fernandez, Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay, Pitts, 2002; Pitts, 2003), which deals with variable binding via permutations and freshness conditions on atoms. Confluence of orthogonal nominal rewriting systems has been shown in (Fernandez, Gabbay, 2007). However, their definition of (non-trivial) critical pairs has a serious weakness so that the orthogonality does not actually hold for most of standard nominal rewriting systems in the presence of binders. To overcome this weakness, we divide the notion of overlaps into the self-rooted and proper ones, and introduce a notion of alpha-stability which guarantees alpha-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and alpha-stability. The new definition of orthogonality and the criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.

In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended lambda-calculus. We first illustrate the technique by showing strong normalisation of a typed calculus that corresponds to natural deduction with general elimination rules. Then we study its explicit substitution version, the type-free calculus of which does not satisfy PSN with respect to reduction of the original calculus; nevertheless it is shown that typed terms are strongly normalising with respect to reduction of the explicit substitution calculus. In the same framework we prove strong normalisation of Sørensen and Urzyczyn's cut-elimination system in intuitionistic sequent calculus.