Inductive-recursive definitions, the topic of this grant, extends inductive definitions by allowing to define a set inductively while recursively defining a function from this set into another type. The main example is a universe, which consists of a set of codes for sets U, defined inductively. It comes together with a function T, defined recursively, which takes each element of U and computes the set it denotes. For instance we have a constructor which introduces a code for the natural numbers in U, and the corresponding recursion rule, which maps this code to the set of natural numbers. In general in induction-recursion the recursively defined function has one computation rule for each constructor of the inductively defined set.
In truly inductive-recursive definitions induction and recursion cannot be separated without some sophisticated encoding (one needs in addition in case of large induction-recursion the existence of large universes). An example is the so called Pi type. The introduction rule says that if we have an element a of type U and a function mapping (T a) to U then we obtain a new element of type U. There is a natural set (the Pi type) to which this new element is mapped by T. We see that the introduction rule for U refers to the recursively defined function T, so U and T need to be defined simultaneously.
In induction-inductive definitions the recursively defined function T is replaced by an inductively defined set which depends on the first inductively defined set. Again both operations cannot be separated without some special encoding.
Inductive-inductive definitions occur naturally in mathematics. An example are Conway's surreal numbers, which were first presented in a popular style book written by Knuth. Here the set of surreal numbers is defined inductively while simultaneously defining a < relation on them inductively. When presenting them, complications arise because the standard framework of mathematics allows only inductive definitions. In some way Conway and Knuth reduce inductive-inductive definitions to inductive definitions, which makes it difficult to understand surreal numbers. We believe that presenting surreal numbers as inductive-inductive definitions is much more intuitive, and allows to define them directly as the simultaneous inductive definition of a set of surreal numbers together with a < relation on it. Another example where inductive-inductive definitions occur naturally are ordinal notation systems. Here a set of ordinal notations (which are transcend numbers) is defined inductively while defining the less than relation inductively.
Induction-recursion occur naturally when one wants to formulate models of type theory inside type theory. The main idea is that one defines a set of types inductively while defining the elements of those types recursively. Induction-induction occurs naturally when defining the syntax of type theory: As an example we consider the rules for defining contexts and the rules for defining the Pi-type as mentioned before:
The rules for deriving contexts correspond to the inductive definition of a set of contexts. Types depending on a context Gamma form a set (Type Gamma), which is defined inductively. Consider the rule for extending a context Gamma by adding a new type A to the context. In dependent type theory, A might depend on Gamma. So the rule takes a context Gamma, an element A of (Type Gamma) and returns a new extended context (Gamma , A). When introducing the Pi type, we take a type A in context Gamma, a type B in the extension of this context by A, and return a type in context Gamma. If we formalise it we take an element Gamma of Context, an element A of (Type Gamma), an element B of (Type (Gamma , A)) and return an element (Pi Gamma A B) in (Type Gamma).
In this example we see that the constructors for Contexts occur in the rules for the constructors for (Type Gamma). This makes induction-recursion very complicated. It means that when defining constructors for (Type Gamma) we can refer on an arbitrary function corresponding to the type of the constructor for context extension. Note that the constructor for context extension has type (Gamma : Context) -> Type Gamma -> Context, so the constructors for (Type Gamma) refer to a function which goes from Context and some other arguments into Context.
In order to get control over this complexity, we used the notion of a Dialgebra. Inductive data types correspond to so called F-algebras. An F algebra consists of a set A (the inductively defined set), a function F mapping sets to sets (which are the arguments of the constructor) and the constructor c : F A -> A. Therefore F-algebra have an operation c which allows to introduce (construct) elements of the set A. Dualising means to invert the direction of the functions. If we dualise F-algebras we obtain F-coalgebras, which have the form e : A -> F A, where e is called a destructor (or an observation). F-coalgebras have an operation which allows to analyse (deconstruct) elements of A. Dialgebras are a combination of both, they are functions f : F A -> G A, where both F and G are functors. The use of dialgebras allows to formulate the introduction and elimination rules for inductive-inductive definitions in a more abstract way. A notion of initiality was defined and we showed (article by Altenkirch, Morris, Nordvall Forsberg and Setzer) the equivalence of the rules for initial algebras based on dialgebras and the elimination rules. This is important since it is not per se clear whether the elimination rules defined are the correct ones. The notion of initiality is more natural, and the fact that both rules are equivalent demonstrates that we have chosen the correct elimination rules.
We generalised the notion of induction-recursion by replacing this concrete split fibration by an arbitrary split fibration. This generalise inductive-recursion to many more general settings. We considered (LICS article by Ghani, Malatesta, Nordvall Forsberg and Setzer), the following generalisations: 1) Universes of setoids (i.e. U is a setoid and T forms families of setoids over U; here a setoid is a set together with an equality relation on it). 2) Universes of relations (i.e. replacing T : U -> D by T : U x U -> Set). 3) Categories of families. 4) Indexed induction-recursion. 5) Containers and indexed containers. This generalises induction-recursion to many more examples. So instead of defining a new calculus for each instance we have one general framework which can be instantiated to each case.
Because of the more categorical approach, we obtained as well a more natural explanation of the rules of induction-recursion. A particular problem is the delta constructor, which allows to extend an inductive-recursive definition by adding on inductively argument. It originated from the informal principles in induction-recursion, but looked quite ad hoc. Using fibrations the rules for delta became very natural.
As mentioned before, initial algebras correspond to inductively defined structures. The rules for List mentioned above express that a List is everything which can be defined using the constructors nil and cons.
Coalgebras are instead sets determined by their elimination rules. For instance the set of streams of natural numbers is the coalgebra with eliminators (deconstructors, observers) head : Stream -> Nat and tail : Stream -> Stream. Intuitively, a stream is any element which allows to define the result of applying head and tail to it. Whereas an element of List is everything which can be constructed, an element of Stream is everything which can be deconstructed. By iteratively applying head/tail to a stream we can unfold it into an infinite list. This shows that final coalgebras allow to define largest fixed points of operators, instead of least fixed foints, as it is the case with inductively defined sets.
Traditionally, in functional programming largest fixed points are representing differently by using codata types. In case of Stream this means that we have a constructor cons taking a natural number, a stream, and constructing a stream. However, while in inductive data types we allow only finitely many applications of a constructor (in a more general setting this will be well-founded many applications) in case of codata types we allow infinitely many applications. Therefore (cons 0 (cons 0 (cons 0 (...)))) is an element of the codata type Stream. We immediately get a problem, namely that this is an infinite term, so we obtain non-normalisation. This is in particular a problem in dependent type theory: During type checking equality between terms needs to be checked, which is done by evaluating terms to normal form and then comparing their normal forms. This is not possible if one allows full evaluation of a stream to (cons 0 (cons 0 ( cons 0 (...)))).
If we instead look at the coalgebra approach, this problem vanishes. The stream consisting of an infinite sequence of 0 is defined as the element zeros of Stream such that (head zeros) = 0 and (tail zeros) = zeros. zeros is in normal form, and therefore a finite object. Its infinite nature is revealed by the fact that one can arbitrarily many times apply head/tail to it, and then unfold it to an infinite stream. Each time one unfolds zeros one has to pay a price, namely to apply a deconstructor to it. That one needs to invest something in each step of unfolding is the reason why one does not obtain a problem with normalisation.
In order to preserve normalisation for codata types and allow for decidable type checking, sophisticated restrictions have to be applied to when a reduction is carried out (i.e. when we can unfold zeros to (cons 0 zeros) ). It has been well known for a long time that because of this the theorem prover Coq violates subject reduction. This means that there is a term t of type A, which has a reduction to a term t' which is not of type A. Note that Coq is now a widely used interactive theorem prover. It has been adopted by Microsoft as "one of their systems" (phrase used by a representative of Microsoft research). It can be used for verifying critical systems in the industrial system SPARK Ada. In Agda, the interactive theorem prover we are using mainly, the subject reduction problem in Coq was repaired by adding severe restrictions to the rules of coalgebras. However, these restrictions are so severe that coalgebras are very difficult to use in Agda.
Because of this we believe that the theory of coalgebras has great advantages. We developed a small programming language in which algebras and coalgebras are completely dual. Algebras are defined by constructors, coalgebras by deconstructors (observations). For algebras the elimination principle is given by pattern matching. In case of List pattern matching means that we can define a function from List into another set, provided we define what to do in case this element is nil and in case it is (cons n l). We introduced the dual of pattern matching, which is called copattern matching. Being the dual of pattern matching, which is an elimination principle, copattern matching needs to be an introduction principle for Coalgebras. It expresses that we can define an element s of type Stream provided we define (head s) and (tail s). Copattern means that for defining s we apply head and tail to it, and then have the obligation of returning a result in each case.
In our joint POPL 2013 paper we introduced a calculus which allowed to combine algebras and coalgebras, patterns, and copatterns, nesting of both and even mixing both. A crucial result is to show that in this calculus we obtain subject reduction. In our RTA-TLCA 2014 we showed that these mixed nested patterns/copatterns can be reduced to unnested ones.
The problem is that the constructor of U for forming U_f refers to a total function which essentially goes from U to U (more precisely from (Fam U) to (Fam U) ). So the reason for introducing U_f as an element of U refers to all of U, which includes the element U_f introduced. This is a form of impredicativity. Impredicativity means here that we have an introduction rule for a set which refers to all of this set, including the element being introduced. Because of this impredicativity there is lot of controversy about whether the Mahlo universe is acceptable in Martin-Loef Type Theory or not.
In our new approach, Anton Setzer and Reinhard Kahle investigated this principle in the context of Feferman's systems of explicit mathematics, which can be considered as an untyped variant of Martin-Loef Type Theory. Setzer and Kahle showed that in explicit mathematics one can define a version of the Mahlo universe which can be considered as predicative (we call it "extended predicative"). The main reason that it is predicative is that the introduction rule for elements in U does no longer depend on a total function f : Fam(U) -> Fam(U). Instead it depends on a partial function f which is sufficient to allow to define a universe U_f closed under f.
The extended predicative Mahlo universe allows to define an elimination rule. Note that an elimination rule is in case of the type theoretic Mahlo universe inconsistent.
We are currently working on extending this setting to proof theoretically much stronger universes such as the so called Pi_3-reflecting universe.
Setzer and Kanso have developed concepts for combining automated and interactive theorem prover in the context of type theory. This allows to verify using SAT solvers and model checkers concrete railway interlocking systems from the British railway system. They were able to show using interactive theorem proving that the resulting systems are safe. A lot of work has been carried out by Kanso in implementing the integration of SAT solvers and model checkers into Agda. It turned out that model checkers could only applied in small examples, whereas the use of SAT solvers was greatly successful, and allowed to fully verify concrete railway interlocking systems.
It turned out that this approach allows to reduce the validation problem. It is a general problem when proving software to be correct to check that the specification against which one checks the software is actually correct. In case of railway interlocking systems one usually proves that the system fulfils certain verification conditions (signalling principles). For instance one verifies that two signals giving access to the same railway segment are not green at the same time. It is not per se clear that if those conditions are fulfilled the system is safe. That this is the case is usually checked manually by domain experts. The problem is that there can be errors in those checks as there can be errors in the original program. Another approach taken is to show that a program refines another abstract program, which is considered to be safe. Again the problem is that the domain experts need to show that the abstract program is safe.
Instead of this approach, Setzer and Kanso introduced a model of the railway system with abstract trains. They were able to show that the system is safe: there are never two trains in the same train segment, so trains do not crash. And if a train passes a set of points, this set of points is locked, so trains do not derail.
There is still a gap between the specification and the requirements (safety of the interlocking system), but the gap is much more narrow. In the approach automated theorem was used to show that the system fulfils certain verification conditions, and interactive theorem proving was used to show that the verification condition imply safety as formulated by the model.
Therefore the approach taken allowed to narrow the validation gap and demonstrated that it is possible to verify real world interlocking systems in the theorem prover Agda.