Descriptional composition is a method to fuse two term transformation algorithms described by attribute couplings (AC, attribute grammars over terms) into one. In this article, we provide a general categorical framework for the descriptional composition based on traced symmetric monoidal categories and the Int construction by Joyal et al. We demonstrate that this framework can handle the descriptional composition of SSUR-ACs, nondeterministic SSUR-ACs, quasi-SSUR ACs and quasi-SSUR stack ACs.
We give a new characterisation of morphisms that are definable by the interpretation of the simply typed lambda calculus with sums in any bi-Cartesian closed category. The TT-closure operator will be used to construct the category in which the collection of definable morphisms at sum types can be characterised as the coproducts of such collections at lower types.
This is the conference version of the manuscript A New Foundation of Attribute Grammars in Traced Symmetric Monoidal Categories.
This is the journal version of the following paper.
We present a unifying solution to the problem of fusion of functions, where both the producer function and the consumer function have one accumulating parameter. The key idea in this development is to formulate the producer function as a function which computes over a monoid of {\em data context}s. Upon this formulation, we develop a fusion method called {\em algebraic fusion} based on the elementary theory of universal algebra and monoids. The producer function is fused with a monoid homomorphism that is derived from the definition of the consumer function, and is turned into a higher-order function~$f$ that computes over the monoid of endofunctions. We then introduce a general concept called {\em improvement}, in order to reduce the cost of computing over the monoid of endofunctions (i.e., function closures). An improvement of the function $f$ via a monoid homomorphism $h$ is a function $g$ that satisfies $f=h\circ g$. This provides a principled way of finding a first-order function representing a solution to the fusion problem. It also presents a clean and unifying account for varying fusion methods that have been proposed so far. Furthermore, we show that our method extends to support partial and infinite data structures, by means of an appropriate monoid structure. (The trip to the conference was partially supported by Kyoto Daigaku Kyouiku Kenkyuu Shinkou Zaidan.)
A semantic formulation of Lindley and Stark's TT-lifting is
given. We first illustrate our semantic formulation of the
TT-lifting in Sets with several examples, and apply it to the logical
predicates for Moggi's computational metalanguage. We then abstract
the semantic TT-lifting as the lifting of strong monads across
bifibrations with lifted symmetric monoidal closed structures.
(This work further develops the example I considered in chapter 4 of
my PhD thesis. The trip to the conference was
partially supported by Saneyoshi Shogakukai.)
We generalise the notion of prelogical predicates to arbitrary simply typed formal systems and their categorical models. We establish the basic lemma of prelogical predicates and composability of binary prelogical relations in this generalised setting. This generalisation takes place in a framework for typed higher-order abstract syntax and semantics.
Simulation relations are tools for establishing the correctness of data refinement steps. In the simply-typed lambda calculus, logical relations are the standard choice for simulation relations, but they suffer from certain shortcomings; these are resolved by use of the weaker notion of pre-logical relations instead. Developed from a syntactic setting, abstraction barrier-observing simulation relations serve the same purpose, and also handle polymorphic operations. Meanwhile, second-order pre-logical relations directly generalise pre-logical relations to polymorphic lambda calculus (System F). We compile the main refinement-pertinent results of these various notions of simulation relation, and try to raise some issues for aiding their comparison and reconciliation.
We extend the study of the relationship between behavioural equivalence and indistinguishability relation to the simply typed lambda calculus, where higher-order types are available. The relationship between these two notions is established in terms of factorisability. The main technical tool of this study is pre-logical relations, which give a precise characterisation of behavioural equivalence. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.
In the past couple of years interest in decompilation has widened from its initial concentration on reconstruction of control flow into well-founded-in-theory methods to reconstruct type information. Mycroft described Type-Based Decompilation and Katsumata and Ohori described Proof-Directed Decompilation. This note summarises the two approaches and identifies their commonality, strengths and weaknesses; it concludes by suggesting how they may be integrated.
We present a proof theoretical method for de-compiling low-level code to the typed lambda calculus. We first define a proof system for a low-level code language based on the idea of Curry-Howard isomorphism. This allows us to regard an executable code as a proof in intuitionistic propositional logic. As being a proof of intuitionistic logic, it can be translated to an equivalent proof of natural deduction proof system. This property yields an algorithm to translate a given code into a lambda term. Moreover, the resulting lambda term is not a trivial encoding of a sequence of primitive instructions, but reflects the behavior of the given program. This process therefore serves as proof-directed de-compilation of a low-level code language to a high-level language. We carry out this development for a subset of Java Virtual Machine instructions including most of its features such as jumps, object creation and method invocation. The proof-directed de-compilation algorithm has been implemented, which demonstrates the feasibility of our approach.
We study a relationship between the Int construction of Joyal et al. and a weakening of biproducts called semibiproducts. We then provide an application of geometry of interaction interpretation for the multiplicative additive linear logic (MALL for short) of Girard.We consider not biproducts but semibiproducts because in general the Int construction does not preserve biproducts. We show that Int construction is left biadjoint to the forgetful functor from the 2- category of compact closed categories with semibiproducts to the 2-category of traced symmetric monoidal categories with semibiproducts. We then illustrate a traced distributive symmetric monoidal category with biproducts B(Pfn) and relate the interpretation of MALL in Int(B(Pfn)) to token machines defined over weighted MALL proofs.
In this paper we propose a new categorical formulation of attribute grammars in traced symmetric monoidal categories. The new formulation, called monoidal attribute grammars, concisely captures the essence of the classical attribute grammars. We study monoidal attribute grammars in two categories: Rel^+ and wCPPO. It turns out that in Rel^+ monoidal attribute grammars correspond to the graph-theoretic representation of attribute dependencies, while in wCPPO monoidal attribute grammars are equivalent to Chirica and Martin's K-systems. We also show that in traced symmetric monoidal closed categories every monoidal attribute grammar is equivalent to the one which does not use inherited attributes.
This thesis proposes a generalisation of pre-logical predicates to
simply typed formal systems and their categorical models. We analyse
the three elements involved in pre-logical predicates --- syntax,
semantics and predicates --- within a categorical framework for typed
binding syntax and semantics. We then formulate generalised
pre-logical predicates and show two distinguishing properties: a)
equivalence with the basic lemma and b) closure of binary pre-logical
relations under relational composition.
To test the adequacy of this generalisation, we derive pre-logical
predicates for various calculi and their categorical models including
variations of lambda calculi and non-lambda calculi such as
many-sorted algebras as well as first-order logic. We then apply
generalised pre-logical predicates to characterising behavioural
equivalence. Examples of constructive data refinement of typed formal
systems are shown, where behavioural equivalence plays a crucial role
in achieving data abstraction.
In this paper, we propose a lambda^S calculus, a simply typed lambda calculus with a rule of type substitution. A distinguishing feature of the lambda^S calculus is to treat type substitution not as meta operation but as logical rule. This yileds a finer equational theory that properly accounts for implicit polymorphism such as the one embodied in ML. We define a type system and an equational theory of the lambda^S calculus and show that it is sound with respect to a categorical semantics on Mitchell and Scedrov's iml-category. We then give a translation from Milner's lambda^let calculus to lambda^S calculus, which reveales that Leroy's type-dicrected boxing and unboxing corresponds to the type isomorphism definable in lambda^S between types with substitution and the corresponding simple types.