Towards a Calculus of Problems in Type Theory with Applications to Relational Rippling

James McKinna

We seek a (search) calculus of problems posed in a type theory with inductive definition. In particular, one which

  • is distinguished from existing presentations of type theory
  • emphasises induction/recursion/case analysis over search oriented analyses which focus on the lambda-Pi fragment of dependent type theory
    • We identify a general form of problem statement which subsumes the \epsilon-expressions of Bundy and Lombart's Relational Rippling (Dagstuhl 9350; July 1995). We further identify a number of rewrite rules in relational rippling as arising from inversion of inductive definitions.

    Induction, recursion, inversion, and even derived case analysis as in the work of McBride, are expressed as left rules in our calculus, whose general from is that of rewriting of subcontexts, similarly to the annotated rewriting of Bundy/Lombart.

    Relational rippling in general is a notationally and semantically complex theory of rewriting annotated \epsilon-expressions. Our hope is, by reanalysing these notions in our new framework, we may simplify as well as learn from, this important search technique. This is very much work in progress.