arXiv subjects
Publications and source records attributed to Ryu Hasegawa.
We give new call-by-value calculi of control operators that are complete for the continuation-passing style semantics. Various anticipated computational properties are induced from the completeness. In the first part of a series of papers, we give the characterization of termination properties using the continuation-passing style semantics as well as the union-intersection type discipline.
We verify a confluence result for the rewriting calculus of the linear category introduced in our previous paper. Together with the termination result proved therein, the generalized coherence theorem for linear category is established. Namely, we obtain a method to determine if two morphisms are equal up to a certain equivalence.
We provide characterization of the strong termination property of the CCV (complete call-by-value) lambda-mu calculus introduced in the first part of this series of the paper. The calculus is complete with respect to the standard continuation-passing style (CPS) semantics. The union-intersection type systems for the calculus is developed in the previous paper. We characterize the strong normalizability of terms of the calculus in terms of the CPS semantics and typeability.
Diagram chasing is not an easy task. The coherence holds in a generalized sense if we have a mechanical method to judge whether given two morphisms are equal to each other. A simple way to this end is to reform a concerned category into a calculus, where the instructions for the diagram chasing are given in the form of rewriting rules. We apply this idea to the categorical semantics of the linear logic. We build a calculus directly on the free category of the semantics. It enables us to perform diagram chasing as essentially one-way computations led by the rewriting rules. We verify the weak termination property of this calculus. This gives the first step towards the mechanization of diagram chasing.