日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

Encoding Type Systems into HyperLMNtal
Alimujiang Yasen, Kazunori Ueda

Type systems are to prevent the occurrence of execution errors during the running of a program. To examine the properties of both type systems and the expressive power of HyperLMNtal, a modeling language
based on hyper-graph rewriting, we encoded polymorphic type systems into HyperLMNtal. Type variables
are represented by hyperlinks and typing rules are represented by rewriting rules which allow simple andeﬀective implementation of type checking. This paper describes the encoding with running examples.

1 Introduction
LMNtal (pronounced “elemental”) is a language
model based on hierarchical graph rewriting thatuses point-to-point links to represent connectivity and membranes to represent hierarchy. LMNtal’s objectives are to serve as a computationalmodel that encompasses diverse formalisms related
to multiset rewriting, concurrency, and mobility,
and to provide a practical programming language
based on hierarchical graph rewriting and its implementation. In recent years, LMNtal was extended
to HyperLMNtal, LMNtal with Hyperlinks, which
is better suited for representing multipoint connectivity in situations where one-to-one connectivity(represented by ordinary links in LMNtal) is impossible to apply directly.
In order to demonstrate the expressive powerof HyperLMNtal to model formal systems, in thepast, various computational models, including the
λ-calculus and the π-calculus have been encoded
into HyperLMNtal [4] [6]. In those encodings, hyperlinks have proved itself as important component which oﬀers straightforward and more eﬃcientmodeling capability. To aim for exploring further
in language development, this paper studies the encoding of type systems.
Alimujiang Yasen, Waseda University, Dept. of Information and Computer Science, Waseda University.
Kazunori Ueda, Waseda University, Dept. of Information and Computer Science, Waseda University.

The λ-calculus has been a subject to extensive research among the programming languages community, since many concepts and technologies whichwere ﬁrst developed on the λ-calculus were transferred to others. It has been a testing ground forprogramming languages research [1]. To go down
further in the development of our programming
language, LMNtal, we want to observe its performance for modeling type systems. We encode the
λ-calculus polymorphic type systems into HyperLMNtal. By doing so, we want to observe how
suitable HyperLMNtal is for the modeling of formal proof systems.
In next section, we will describe the syntax andother features of HyperLMNtal quickly. Then,
there will be a short section about type systems.
The encoding will be explained in the next section.
The ﬁnal section is dedicated to conclusion.

2 LMNtal and HyperLMNtal Overview
LMNtal views that computation is manipulationof diagrams, which in our case consists of (i) atoms,(ii) links for one-to-one connectivity, and (iii) membranes that can enclose atoms and other membranes and can be crossed by links. Connectivity and hierarchy are two major structuring mechanisms in LMNtal as well as in the real world. The
purpose of LMNtal is to provide a programmingand modeling language which enables representing
and manipulating directly both real-world and cyberworld applications [5].
The two syntactic categories, link names (de-(Process) P ::= 0 | p(X1 ,...,Xm ) | P,P | {P } | T:-T
(Process template) T ::= 0 | p(X1 ,...,Xm ) | T,T | {T } | T:-T | @p | $p
Table 1

Syntax of LMNtal.

noted by Xi ) and atom names (denoted by p)
are presupposed. Processes are the principal syntactic category and consist of hierarchical graphs
and rewrite rules. Being a model of concurrency,
LMNtal uses the terms (hierarchical) graphs andprocesses interchangeably. 0 is an inert process,p(X1 ,...,Xm ) (m≥0) is an atom with arity m, P,P
is parallel composition, {P} is a cell formed by enclosing P by a membrane { }, and T:-T is a rewriting rule. The two T ’s are called the head and the
body of the rule, respectively. A rewrite rule is subject to several syntactic conditions. Most notably,
a link name occurring in a rule must occur exactly
twice in the rule.
The reserved atom name, ‘=’, is called a connector. The process X=Y connects the other end oflink X and the other end of the link Y. A rule context, denoted by @p, matches a (possibly empty)
multiset of all rules within a membrane, while aprocess context, denoted by $p, is to match processes other than rules within a membrane.
An abbreviation called a term notation is frequently used during LMNtal programming. It allows an atom b without its ﬁnal argument to occur
as the k th argument of a. For instance, f(a,b) is thesame as a(A),f(A,B),b(B). A list with the elements
Ai ’s can be written as X =[A1 ,...,An ], where X isthe link to the list. Some atoms such as ‘+’ arewritten as unary or binary operators.
Example 1 This example demonstrates the use ofprocess contexts:

Here, the ‘/’ notation is the stability constraint: acell suﬃxed by a ‘/’ in the head of a rule can matcha cell that cannot be reduced further. In this example, when the ﬁrst cell has been stabilized (ﬁrstcell rule set @z cannot apply further), the rule set@q from the second cell will be applied to process$p within the ﬁrst cell.
LMNtal has provided a module system which isuseful in cases where program ﬂow is complex. A
module is a set of rules packaged in a membranewith a module name deﬁnition.
{module(module name), RuleSet}
The RuleSet is made available only when it isloaded outside the membrane.
Example 3{
module(seq).
seq.run( data{$p},rule{@q} ):- seq.run( data{$p,@q} ).
}.
seq.run( data{a(3),b(2)},rule{ a(M),b(N):-a(M+N). } ).

In this example, the rule set is applied to datawith taking advantage of the module. Using modules with process templates together, controlling ofcomplex program ﬂow can be achieved. The result
is:{+X,$p},{+X,$q} :- {$p,$q}.
seq.run( data{a(5)}).
This says that two cells that are connected by alink (X, which connects two unary atoms +) will
be fused.
Example 2 In order to apply a new rule set to aprocess P, one can write{$p,@z}/,{@q} :- {$p,@q}.

For concise representation of multipoint connectivity, hyperlinks have been introduced into LMNtal and extended it to a hierarchical hypergraphrewriting model, HyperLMNtal. Hyperlinks are
essential for our encoding. Hyperlinks are local
names shared by any number of atoms [2].
.

H :- new($x)| B.
H :- hlink($x) | B.
H :- .......
| $x >< $y, B.
H :- num($x,$n) | B.

A local fresh name can be created by a new guard
constructs as shown (ﬁrst line of the above code).
To check if an argument of an atom is a hyperlink,
hlink (second line) can be used. Fusion (third line)
may be the most characteristic operation on hyperlinks. Two hyperlinks $x and $y are merged into
one. Another operation is to obtain the cardinalityof a hyperlink by using num ($n is bound to thecurrent cardinality of $x). All hyperlinks occur inthe head of rewriting rule ‘H’, except the ﬁrst line.

type schemes. The “Γ ok” indicates that the free
type variables of each type scheme are contained inΓtv , which is a ﬁnite set of type variables. Γta is a
type scheme assignment function, i.e. a ﬁnite function mapping some variable, xi , to type scheme, σi .
The A in the let typing rule is a set of type variables
which occur in τ1 .

4 Encoding Type Systems
The encoding went through two phases. In theﬁrst phase, we encoded constraint type checking of
the simply typed λ-calculus. In second phase, we
extended our encoding with let polymorphism. In
the ﬁrst subsection, we will discuss general issues.
In the second subsection, we will present the ﬁrst
phase of our encoding. The third subsection will
focus on the encoding of let polymorphism.

3 Type Systems
The main goal of our encoding is demonstrating
the modeling power of HyperLMNtal. By doing so,
we could have new understanding about the beneﬁts of HyperLMNtal as well as ideas of further
improvement. We have chosen constraint typing of
simply typed λ-calculus as the subject to our encoding. Thereafter, we will extend it to a more
complex type system with let polymorphism.
Since those are well-known formalisms, only toremind the reader in case, typing rules are given.

(var Â)
(abs)

(app)

Γ ` x : τ if Γ ok, f tv(τ ) ⊆ Γtv
and σ Â τ for some (x : τ ) ∈ Γta
Γ, x : τ1 ` M : τ2

Γ ` λx(M ) : τ1 → τ2
Γ ` M1 : τ1 → τ2

∩

(let)
(nil)
(list)

if x 6∈ dom(Γta )Γ ` M2 : τ1

Γ ` M1 M2 : τ2

if A Γtv = ∅ and x ∈/ dom(Γta )Γ, x : ∀A(τ1 ) ` M2 : τ2
A, Γ ` M1 : τ1
Γ ` letx = M1 in M2 : τ2
Γ ` nil : τ list if Γ ok and f tv(τ ) ⊆ Γtv
Γ ` M1 : τΓ ` M2 : τ listΓ ` M1 :: M2 : τ list
Table 2Typing rules.

Here, the f tv(τ ) is a set of free type variables of

4. 1 Issues
To model the process of type checking in HyperLMNtal, we have to consider following:
1. (Expression) Type checking involves terms,
types, derivation and so on. Besides, thoseinteract with each other, especially during
derivations. We need to come up with a concise way of representing them by using atoms,
membranes and links.
2. (Relation) During type checking, terms are
subject to derivation. Constraints, generated
during the derivation, are subject to uniﬁcation. One type might occur in many terms,
and typing context may be shared by multiple
terms.
3. (Sharing) It can be seen from typing rulesthat during derivation, type contexts are always delivered or extended to further derivation. There should be resource sharing or copying.
4. (Sequentiality) The type checking process
is a combination of derivation and uniﬁcation.
Unfortunately, in LMNtal, controlling program
ﬂow is not as easy as doing it in imperative programming languages.
5. (Fresh variables) The derivation may needto create fresh type variables.
All those are to be considered simultaneously.
For the expressions, atoms in HyperLMNtal would
be a good choice. To represent the relation be-tween terms and constraints, links are the best solution. To represent complex relation between multiple terms, hyperlinks will be used. The sharedresources can be stored in membranes with atoms,
and templates could make it easy to copy if needed.
To control the programming ﬂow, we will utilize
templates with modules. For reﬂecting relationship between type variables, hyperlinks is a natural
choice. Hyperlinks are always created fresh. Also,
equality checking can be performed on hyperlinks,
which is very useful for our encoding.
4. 2 Encoding of Type Checking
In this section, we will consider the ﬁrst phase of
our encoding. We pick a simple term and follow its
type checking process. Our idea will be presented
alongside this process. The most simple case might
be the type checking of the following term.
Γ ` λx.x : T
We want to ﬁnd out type T . That term is represented by the following code.
sequent(tenv{}, type(abs(x, x), !T ))Here, sequent represents a single conclusion judgment of a typing rule. The ﬁrst argument of
sequent is tenv{}, which stands for an empty typing context. The second argument is a type atomwhich has two arguments. In that atom, the ﬁrst
argument is a term subject to type checking andsecond one is a type which is represented by a hyperlink. That hyperlink always points to computed
type of the term. The notation ‘!’ is another way
to create a hyperlink, the same with the new construct.
A derivation in a given type system is a tree of
judgments, where each judgment is obtained fromthe ones immediately above it by some typing ruleof the system. Each type rule is written a as anumber of premise judgments above the horizontal line, with a single conclusion judgment below
the horizontal line. In our encoding, the typing ruleabs which is applicable to the above term is represented as:abs@@ sequent(G, type(abs($x, M ), T )):unary($x) | add env(G, $x, !T 1, E),

sequent(E, type(M, !T 2)), cs(T, arrow(T 1, T 2)).
Rewriting rules can be preﬁxed by a rule name,such as abs by using the ‘@@’ mark. The LHS
of a typing rule is a single judgment, which corresponds to the conclusion judgment in the typing
rule. The unary in the guard ensures that $x is aunary atom. The add env takes a type context G,
extends it with a pair, a variable $x and its supposed type T 1 (which is newly created). The extended type context can be reached by E. A new
sequent will be created, which is for type checkingof M . And the relationship between types in typing rules is reﬂected by creating a constraint, whichis represented by a cs atom. The cs reads as “thetype T is a function type, T 1 → T 2.”
To ensure type context sharing and extending in
those rules, auxiliary rules for copying and extending type contexts are implemented (one of themis add env). The implementation of other typing
rules utilizes similar representation as seen in theabove code. The relationship of types is reﬂected bygenerating cs style atoms. The type context is represented by a membrane which encloses atoms with
the name type, which illustrates a mapping from avariable to its type. Extending a type context adds
a new mapping. In our var rule implementation,
if we have found two mappings within a type context, those have a common variable and diﬀerent
types, then typing rule var creates new cs whichsays those two types are equal.
During the derivation, applying rules createsmany cs atoms, which are subject to uniﬁcation
after derivation is completed. After derivation isover, redundant data will be removed by using auxiliary rules.
The uniﬁcation algorithm is implemented to solve
a set of constraints (set of cs) to ﬁnd out the typeof the given term. We treat them from the viewpoint of a set of equations [3]. In our implementation, data sets and rule sets are separated. A given
term for type checking is placed in one membrane,
derivation rules and uniﬁcation rules are placed in
the next membrane, occur check rules are in another membrane. This has two major advantages:
one is to control sequentiality of type checking (recall Example 3), another is to have clean encoding.
The occur check rule set is supplied to data right after the uniﬁcation. It stops the program from run-ning further once there is an unsolvable equation
detected. Parts of uniﬁcation rules are as below.
cs(!T 1, !T 2) :- !T 1 == !T 2 |.
cs(!T 1, !T 2) :- !T 1\ = !T 2 | !T 1 ><!T 2.
Thus, we will have a set of equations (we change
the atom name cs to sub after each of them passed
occur checking without failing), which represents
the type of the given term, as below.
sub(!H16, arrow(!He, !He)).
So far, we have presented our work on the ﬁrst
phase of this work. The next subsection will present
an encoding of let polymorphism. (To manage
space, most of the encoding are not displayed.)
4. 3 Let Polymorphism
The encoding of let polymorphism is much morechallenging, due to several reasons.
1. (Type scheme) Until now, our type context
only includes a kind of mapping from variables
to types. Adding new mapping pairs, fromvariables to type schemes, will add extra complication and aﬀect our uniﬁed structures, suchas judgment, type context and so on.
2. (Sequentiality) The let typing rule asks us
to perform type checking twice. This requires
more complex sequentiality which leads to difﬁculty for managing program ﬂow.
3. (Occurrences ) Keeping track of the occurrences of a let deﬁnition inside a let body also
adds complexity.
4. (Instantiation) To interpret diﬀerent types
for each occurrence of a let deﬁnition, we haveto come up with a delicate way of instantiation.
It seems we cannot avoid more complex sequentiality, but we can manage it by using template andmodule in HyperLMNtal. Another rule set, which
controls programmed ﬂow, is added. Each obvious step of type checking is marked with special
atoms which are used as tags to detect which ruleset should be supplied once the previous process
been stabilized. The occurrences of a let deﬁnition
can be counted by adding an extra rule. In this way
we know how many instantiations of a let deﬁnition
type we should have.

The instantiation is a major problem. The set of
equations representing the type of a let deﬁnition
have to be copied as many times as needed. But
the hyperlinks (present in many terms) cannot be
copied, because a hyperlink always maintains thesame hyperlink name whenever it appears.
Fortunately, HyperLMNtal has provided somefeatures which will simplify our solution. One isthat a hyperlink can be created with an attribute,
another is that there is a type constraint which will
help us copy a hypergraph connected by hyperlinks
with a speciﬁc attribute and each copy of a hypergraph will be diﬀerent from others.
init.
init:- !X : 1 | a(!X).
a($hl):- hlground($hl, 1) | a($hl), a($hl).
The rule in second line creates a hyperlink named
X with attribute ‘1’. The second rule in thirdline has a constraint in the guard, hlground, whichtakes a hyperlink and an attribute. The hlgroundensures that two hypergraphs in the two atoms,a($hl), after copying, will have diﬀerent hyperlink
names but the same attribute (maintain ‘1’).
The above features lead to very interesting encoding of let polymorphism. It is observed in let
typing rule that a set A of variables (those variables
appear in type of let deﬁnition, but not in the typecontext, recall let typing rule), is generated during
type checking of the let deﬁnition. Thus, the set
A only includes hyperlinks we wish to copy. Other
hyperlinks which are created during type checkingof let body never appear in the set A.
We have found a novel solution. We assign different attributes to hyperlinks which are created at
diﬀerent stages of let type checking. All hyperlinks
created during type checking of the let deﬁnition
are assigned the same attribute, while hyperlinks
created during type checking of let body, are assigned another attribute. This mean we are usinga hyperlink attribute to refer to a set of hyperlinks.
We can copy hyperlinks with an attribute by usinga hlground constraint in the guard of a rewriting
rule. Therefore, we can remove the set A from ourimplementation of the let typing rule as long as wehave the records of the attributes.
Without the presence of the set A, we no longer
need the type scheme in let rule implementation.

What we only need to do is add a few rules whichchange an attribute value, which is assigned to eachhyperlink when it is created, at the time when typechecking of let deﬁnition is over.
With the help of hyperlink attributes and thehlground constraint, only minor changes are added
to merge let type checking to the ﬁrst phase of our
encoding.

5 Discussion and Conclusion
Those encoded type systems are well known classic systems. By encoding those type systems, wewant to ascertain that HyperLMNtal, a language
model based on hierarchical graph rewriting, is expressive enough to model complex systems.
Another ﬁnding is that HyperLMNtal is strong
enough to model and help us to study formal proof
systems. Besides, this work helped us to realize
some potential problems in our language implementation. There are more than forty rules in our encoding, of which only typing rules come from direct translation. Many auxiliary rules for type context related operations, sequentiality control andoccur checking are implemented additionally. This
reﬂects the fact that encoding of type systems are
not an easy task.
There are several interesting ﬁndings that canbe learned from this work. First, hyperlink area very natural way to represent multi-point connectivity. This fact came from observing implementation of type rules and uniﬁcation, which areconveniently encoded with hyperlinks. Second, hyperlinks with attributes greatly simpliﬁed our en-

coding of let polymorphism. With hyperlinks withattributes, we are able to remove an explicit typescheme from our implementation, since an attributeis used to mark a set A of variables (see let rule).
Thus, we avoided bringing too many changes to theﬁrst phase of encoding.
In the past, some computational models were encoded into (Hyper)LMNtal. This is the ﬁrst timethat HyperLMNtal is used to model a type system. We plan to encode more type systems todemonstrate the value of HyperLMNtal as a unifying model.
References[1] Benjamin C. Pierce, Types and Programming
Languages, The MIT Press, Cambridge, Massachusetts, 2002.
[2] Kazunori Ueda and Seiji Ogawa, HyperLMNtal:
An Extension of a Hierarchical Graph Rewriting
Model. Künstliche Intelligenz, 26(1), 2012, pp. 2736.
[3] Alberto Martelli and Ugo Montanari, An Eﬃcient Uniﬁcation Algorithm. ACM Transactions on
Programming Languages and Systems, 4(2), 1982,
pp. 258-282.
[4] Kazunori Ueda, Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting. In Proc.
19th International Conference on Rewriting Techniques and Applications (RTA 2008), LNCS 5117,
Springer, 2008, pp. 392-408 .
[5] Kazunori Ueda, LMNtal as a Hierarchical Logic
Programming Language. Theoretical Computer Science, 410(46), 2009, pp. 4784-4800.
[6] Kazunori Ueda, Towards a Substrate Frameworkof Computation. To appear in Concurrent Objects
and Beyond (COB 2012), LNCS, Springer, 2013 (26pages).