Generalized inference systems have been recently de ned to overcome the strong dichotomy between inductive and coinductive interpretations. They support a exible form of coinduction, subsuming even induction, which allows one to mediate between the two standard semantics. Recently, this framework has been successfully adopted to dene semantic judgments which uniformly model nite and in nite computations. In this communication, we survey these results and outline directions for further developments.
In operational semantics, nite behaviour can be easily modelled by inductive
techniques. That is, we can de ne a judgement c ) r , meaning that the
evaluation of the con guration c terminates with nal result r , by an inductive1
inference system, either on top of a small-step relation [
However, modelling in nite behaviour is not that easy. The simplest in nite behaviour we may want to model is divergence itself, which can be formalized by a judgement c ) 1. Such judgement is usually de ned at the meta-level in small-step semantics, saying that c ) 1 holds if there is \an in nite sequence of steps" starting from c. In big-step style the situation is worse: non-terminating and stuck computation cannot be distinguished.
In literature, several approaches to face this issue can be found: divergence is
modelled by a separate coinductive de nition [
However, modelling divergence is not enough to formally reason about
nonterminating programs, since we want in some cases richer information about their
behaviour. Hence we need more sophisticated semantics, which are even more
di cult to de ne. An example is trace semantics, where, in addition to the nal
? Special thanks go to Elena Zucca and Davide Ancona for their useful comments and
the review of this communication.
1 Valid judgements are those having a nite derivation.
result, a trace of observed events is produced. Also in this setting there is some
literature [
All these approaches are not completely satisfactory because they require
ad-hoc changes to the natural de nition. A possible alternative, shown in [
In this communication we summarize the sresults obtained by this approach and we outline possible directions for further developments. More precisely, in Section 2 we brie y present the framework of generalized inference systems, and in Section 3 we deal with their application to in nite behaviour. 2
In this section we brie y introduce inference systems [
Assume a set U called the universe, whose elements are called judgments. Pr An inference system I consists of a set of (inference) rules, which are pairs , c with Pr U the set of premises, c 2 U the consequence (a.k.a. conclusion). A rule with an empty set of premises is also called an axiom. A proof tree is a tree whose nodes are (labeled with) judgments, and there is a node c with set of
Pr children Pr only if there exists a rule .
c
We can associate with an inference system I a function FI : }(U ) ! }(U ),
monotone on the complete lattice }(U ) ordered by set inclusion. We de ne the
iinntdeurcptrievteaitniotnerpJrIeKtcaotinidonasJItKhinedgarseathteestleasxtedxpeodinptoionft FofI ,FwI,haicnhd etxhiestcotihnadnukcstivtoe
Tarski's theorem [
In some cases neither of these two approaches yields the expected semantics. Let us consider an example: let N1 be the set of nite and in nite lists of natural numbers. The predicate maxElem(l; x), stating that x 2 N is the maximum of l 2 N1, is de ned as follows: maxElem(x; x) maxElem(l; y) maxElem(xl; z) z = maxfx; yg The inductive interpretation is not enough, because the predicate would be unde ned for all in nite lists. Indeed, in order to compute the maximum of an in nite list, we need to inspect all its elements, and this clearly cannot be done in a nitely many steps. On the other hand, the coinductive interpretation does not work as well: for the list L containing only 1s, we can derive by an in nite proof, applying in nitely many times the second rule, the judgement maxElem(L; n) for all n 1. That is, the coinductive interpretation is not sound, since it allows us to derive too many judgements. Hence, we need something in the middle between the (least) inductive interpretation and the (greatest) coinductive one.
In [
De nition 1 (Inference system with corules). An inference system with corules, or generalized inference system, is a pair hI; Icoi where I and Ico are inference systems, whose elements are called rules and corules, respectively.
Pr Corules are written and a corule with empty premises is called coaxiom.
c Analogously to rules, the meaning of corules is to derive a consequence from the premises. However, they can only be used in a special way, as described below.
The interpretation of an inference system with corules hI; Icoi is de ned in two steps: 1. First, we consider the inference system I [ Ico where corules can be used as rules as well, and we take its inductive interpretation JI [ IcoKind. 2. Then, we take the coinductive interpretation of the inference system obtained co ind.
from I by keeping only rules with consequence in JI [ I K Altogether, we get the following de nition.
De nition 2 (Interpretation). Let hI; Icoi be a generalized inference system. Then, its interpretation JI; IcoK is de ned by JI; IcoK = JIjJI[IcoKind Kcoind where, for a subset S U , IjS denotes the inference system obtained from I by keeping only rules with consequence in S.
It can be shown that JI; IcoK is a xed point of FI , in particular the greatest xed point below the least xed point of FI[Ico . From this fact, we also get a generalization of the coinduction principle to our setting, called the bounded coinduction principle, which is a proof technique to show the completeness of a de nition.
An interesting fact is that both the inductive and the coinductive interpretations are subsumed by this generalized semantics. Indeed, if Ico = ;, we get the former, while if Ico contains a coaxiom for each c 2 U we get the latter.
In proof-theoretic terms, JI; IcoK is the set of judgments which have an arbitrary (well-founded or not) proof tree in I, whose nodes all have a well-founded proof tree in I [ Ico.
Considering again the above example, by adding the coaxiom
maxElem(xl; x) we get the expected semantics. Intuitively, the coaxiom forces the result to belong to the list. Then, from the standard inference system we get that maxElem(l; x) i x is an upper bound of l, and from the coaxiom x must belong to l, hence x must be the maximum of l.
We started studying how corules can be used to model in nite behaviour [
In [
Hence, to capture the intended semantics, we designed appropriate corules. Intuitively, corules specify when we are allowed to use coinduction. In this case, they shoud be applied only to derive divergence; thus we added a coaxiom with conclusion e ) 1 for each e.
Having de ned big-step semantics including divergence, we started studying how to prove properties of non-terminating programs. The rst one we have considered is type soundness, which can be rephrased as completeness of the big-step semantics with respect to the type system, hence it can be proved using a variation of the bounded coinduction principle.
In [
We have considered two example languages: a -calculus with output e ects and an imperative FJ-like language with I/O primitives; in the former case traces contain printed values, in the latter I/O events. As for the simpler case of divergence, we have added rules for divergence propagation and appropriate corules, which in this case are more complex. Consider for instance those for the -calculus: (co-empty)
(co-out) e ) h1; "i
e ) hv ; oi out e ) h1; o v o1i 2 There is no axiom with conclusion e ) 1 for some expression e. where " is the empty trace, o a nite trace, o1 a possibly in nite trace, and trace concatenation. As before, corules allow coinduction only to derive diverging judgements. Coaxiom (co-empty) deals with diverging computations producing a nite trace, namely, computations printing some values and then diverging without producing any other output, as expressed by the empty trace in the conclusion. Corule (co-out), instead, deals with computations producing an in nite output trace: intuitively, those which evaluate in nitely many output expressions. In such cases the in nite trace is unique, hence the corule allows any trace in the conclusion, but it checks that the output expression is actually evaluated, that is, its argument must converge.
The above considered semantics exhibit common patterns, both for rules and corules. An interesting and promising direction for further work is to abstract these patterns to a more general setting, to study general properties of semantics de ned by inference systems with corules.
This common structure can be summarized as follows: all semantics with corules contain standard rules for converging computations, rules for divergence propagation and corules to allow coinduction only to derive divergence. Furthermore, the de nition of semantics including divergence seems to be driven by the standard semantics for converging computations.
Following these remarks, what we plan to do is to de ne a canonical construction that, starting from a standard big-step semantics for nite computations, produces an extended semantics including diverging computations as well. We would like such general framework to subsume trace semantics and, more generally, other kinds of semantics describing the observable behaviour of programs.
To this end, we need to identify a general algebraic structure for observations, and to de ne a general notion of semantics with observations, that is, a semantics which, in addition to the nal result, produces also an observation, describing the observable behaviour of the program.
Then, the canonical extension will require to introduce a new result for divergence, extend observations (and their structure) to include in nite ones and to de ne appropriate divergence propagation rules and corules.
To guarantee the correctness of the proposed construction, we plan to compare the resulting semantics with more standard techniques, such as labelled transition systems. This comparison could be a parametric proof of equivalence, which, starting from suitable hypothesis on the semantics for nite computations, proves the equivalence of the entire semantics.
Other possible, more long-term, directions for further developments are a
deeper comparison with de nitional interpreters, notably those based on the
partiality monad [