Type theory w/ custom reduction rules in inductive types

Stream: Type theory

[Brandon Brown]

I've been exploring different ways of constructing the same type, e.g. the integers using a regular inductive type, subtype or quotient type. Each has its pros and cons.

Constructing the integers as an inductive type derived from the natural numbers, e.g.

inductive int : Type where
| pos : Nat → int
| neg : Nat → int

Is convenient because it's a regular inductive type and it's therefore easy to define functions with it. One minor con is that there are two zero representations: pos zero and neg zero

Alternatively, one can use a subtype of an inductive type that doesn't depend on Nat such that only a restricted subset of representations are used, namely where succ $ pred a = a and pred $ succ a = a

inductive pInt : Type where
| zero : pInt
| succ : pInt → pInt
| pred : pInt → pInt

def is_norm (a : pInt) : Bool :=
match a with
| zero => true
| succ (pred a) => false
| pred (succ a) => false
| succ zero => true
| pred zero => true
| succ a => is_norm a
| pred a => is_norm a

def int := {x : pInt // is_norm x}

This version of the integers doesn't have cons of the first presentation, e.g. there is a unique zero, but now it has the con that you have to carry around a proof that it is in normal form. So it's quite unpleasant to have to do :

#reduce int.add (Subtype.mk zero.succ.succ rfl) (Subtype.mk zero.succ.succ rfl)

instead of just:

#reduce zero.succ.succ + zero.succ.succ

like you can do with a regular inductive type.

I suppose I could create a notation that makes this easier:

notation "↓" a => ((Subtype.mk a rfl) : int)
#check int.add (↓zero.succ.succ) (↓zero.succ.succ)

All of this preface is to ask, is there a type theory where one can define reduction rules within an inductive type? I'm thinking it would look something like this

inductive pInt : Type
| zero : pInt
| succ : pInt → pInt
| pred : pInt → pInt
where
| succ $ pred a => a
| pred $ succ a => a

such that anytime I tried to a create term that matched my custom reduction patterns, it would automatically get reduced such that it would be impossible to create a term with a pattern like zero.succ.pred as it would automatically get reduced at the Kernel level to zero, e.g.

def some_int : int := zero.pred.succ
#reduce some_int -- zero.succ

This new type forming mechanism would function just like my int subtype, except that now I don't need to prove that some int is in normal form as it is impossible to construct a non-normal int and I can use it as I would a regular inductive type. Note, to my eye this is different than a quotient or a higher-inductive type as there is no notion of equality here, I'm not intending to define equalities, I'm defining reductions.

[Mario Carneiro]

One minor con is that there are two zero representations: pos zero and neg zero

Rather than a con, I would call that evidence that this type is not the integers. The integers do not have two values that are both zero and not equal to each other. As you probably know, the real lean definition of the integers uses the two-constructor approach but shifts the neg constructor so that it doesn't cover zero (leading to the cumbersome name neg_succ_of_nat).

[Mario Carneiro]

Brandon Brown said:

This version of the integers doesn't have cons of the first presentation, e.g. there is a unique zero, but now it has the con that you have to carry around a proof that it is in normal form. So it's quite unpleasant to have to do :

#reduce int.add (Subtype.mk zero.succ.succ rfl) (Subtype.mk zero.succ.succ rfl)

instead of just:

#reduce zero.succ.succ + zero.succ.succ

like you can do with a regular inductive type.

That isn't really a problem once you have built the API. You just define int.zero and int.succ so that zero.succ.succ : int, and define int.add and make it an instance of has_add so that x + y : int works. As long as you do these things zero.succ.succ + zero.succ.succ can be made to work regardless of how the type is actually defined

[Mario Carneiro]

Brandon Brown said:

All of this preface is to ask, is there a type theory where one can define reduction rules within an inductive type? I'm thinking it would look something like this

inductive pInt : Type
| zero : pInt
| succ : pInt → pInt
| pred : pInt → pInt
where
| succ $ pred a => a
| pred $ succ a => a

First, this is necessarily a higher inductive type (HIT) because you have an inductive type with some equalities. However, if you use HITs a la HoTT, you still won't get reduction rules because your equalities are defeqs rather than paths which freely generate the equality type on the inductive. I have not seen any type theory that validates this sort of thing, and while this specific example can be proved to exist I can already see lots of ways to prove false with an unrestricted mechanism of this form. What does the recursor for this type even look like?

[Nick Scheel]

If you want to read more about (the subtleties of) defining integers as higher inductive types, there’s a whole paper on it: https://arxiv.org/abs/2007.00167

[Kevin Buzzard]

There's also a recent talk by Thorsten Altenkirch which I think Alex Best posted a YT link to recently, which to be honest just made me feel that HoTT was totally unsuitable for defining regular mathematical objects (I'm on the Android app and can't figure out how to search for posts by a user)

[Mario Carneiro]

For the lazy: https://www.youtube.com/watch?v=Fov95A2bGDI

[Scott Morrison]

"Making the integers incomprehensible"

[Brandon Brown]

Thanks @Mario Carneiro for the point by point.I’m familiar with the integers as a HIT paper and presentation. I didn’t think it would be quite like a HIT because I didn’t think I was postulating equality. That is, I want something of the form of succ $ pred a to be immediately reduced to ‘a ‘ without equating them. If they’re equal then I could do the reverse and turn ‘a’ into succ $ pred a and I don’t want that possibility. But in any case, I can see how making a better interface for subtypes can solve most of my issues.

[Mario Carneiro]

succ(pred a) has to be a term because succ and pred are functions. If one reduces to the other then they are necessarily equal by rfl

[Mario Carneiro]

It's not crazy to have a reduction rule like that, that's more or less how reduction of recursive definitions on inductive types works

[Mario Carneiro]

If you have

def foo : nat -> nat
| 0 := 0
| (succ n) := foo n + 2

then foo (succ n) ~> foo n + 2, i.e. there is a left-to-right reduction, but this implies that foo (succ n) = foo n + 2 is an equality that is provable, and it's proof is rfl

[Mario Carneiro]

Postulating the equality is a bit different from postulating a defeq, which is a bit different from postulating a reduction

[Mario Carneiro]

HITs in HoTT postulate the equality, and as a result they have to deal with coherence hell (see the integer HIT talk)

[Mario Carneiro]

Postulating the defeq, or the reduction, have the problem that the recursor can't be expressed without "defeq hypotheses", which is not a thing that exists in lean. Cubical type theory is based on a type Path A a b which is like the subtype {f : [0,1] -> A // f 0 = a /\ f 1 = b}, except the two equalities are defeqs. So the introduction and elimination rules for the type have to be built into the foundations, and there are a ton of novel consequences

[Mario Carneiro]

So I can believe that cubical type theory would either be able to simulate such a defeq-HIT or could be extended to support one. I'm sure they would be interested to investigate something like that

[Mario Carneiro]

Postulating a reduction is more or less the same thing, except it has additional consequences for the decidability of defeq and strong normalization / canonicity. For example you would want to know that every closed term of type int reduces to succ^n 0 or pred^n 0, and the reduction rules are confluent and don't cause infinite loops. As far as I know there is no general method for checking arbitrary rules supplied by the user to ensure these properties, you basically have to redo the analysis with each new reduction rule that is added. I don't think your proposed reduction rules for the integers are problematic, but it's always hard to tell if there won't be some problematic interaction with a corner of the type theory you weren't thinking about

[Brandon Brown]

Very interesting, thank you- maybe some future proof assistant will have this. For now, I will use a subtype

[Eric Bond]

This is perfectly valid Cubical Agda.
https://agdapad.quasicoherent.io/#PassionateOutsidesDecorateGradually

{-# OPTIONS --cubical #-}
module cube where

open import Data.Nat

open import Cubical.Foundations.Prelude

data Int : Set where
    pos : (n : ℕ) -> Int
    neg : (n : ℕ) -> Int
    z : pos 0 ≡ neg 0

[Eric Bond]

Also doable in Arend
(both languages are based on cubical type theories)

[Reid Barton]

But ≡ is "typal" not definitional equality in Agda, right?