how to hack around the lack of coinduction

Stream: lean4

[awalterschulze]

I was wondering if there is a way to hack this type to not require coinduction or unsafe

Here is the type defined in Agda using coinductive:

record Lang (P : ◇.Lang) : Set (suc ℓ) where
  coinductive
  field
    ν : Dec (◇.ν P)
    δ : (a : A) → Lang (◇.δ P a)

Here is my attempt to redefine the type in Lean, using unsafe:

unsafe
inductive Lang {α: Type u} (R: Language.Lang α): Type (u) where
  | mk
   (null: Decidability.Dec (Calculus.null R))
   (derive: (a: α) -> Lang (Calculus.derive R a))
   : Lang R

Without unsafe, I get the following error (kernel) arg #4 of 'Automatic.Lang.mk' contains a non valid occurrence of the datatypes being declared

This is part of a project reprove the following Agda paper in Lean: "Symbolic and Automatic Differentiation of Languages - Conal Elliott"

The full project is here: https://github.com/katydid/symbolic-automatic-derivatives

The problem is also described here with slightly more detail: https://github.com/katydid/symbolic-automatic-derivatives?tab=readme-ov-file#coinduction--termination-checking

[awalterschulze]

We have made some progress, but now we run into termination checking issues, see
https://github.com/katydid/symbolic-automatic-derivatives/pull/2

[Edward van de Meent]

how should equality on a coinductive behave?

[awalterschulze]

I am quite the coinduction noob, so not sure

[Edward van de Meent]

that makes two of us, i guess :sweat_smile:

[awalterschulze]

So now we can define a "coinductive" type without unsafe

inductive Lang {α: Type u} : Language.Lang α -> Type (u+1) where
  | mk
    (null: Decidability.Dec (Calculus.null R))
    (derive: (a: α) -> Lang (Calculus.derive R a))
    : Lang R

But when we instantiate it, we need to use unsafe again

-- ∅ : Lang ◇.∅
unsafe
def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
  -- ν ∅ = ⊥‽
  (null := Decidability.empty)
  -- δ ∅ a = ∅
  (derive := fun _ => emptyset)

Otherwise we get the error:

fail to show termination for
  Automatic.emptyset
with errors
failed to infer structural recursion:
Not considering parameter α of Automatic.emptyset:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, 'Automatic.emptyset' does not take any (non-fixed) arguments

[Jannis Limperg]

These termination issues seem to be inherent to the task. The coinductive Lang type is an infinitely branching tree of possibly infinite depth and the emptyset value has infinite depth, so its construction cannot terminate.

Maybe you can hack around this with some sort of fuel-based construction: define the type of Lang trees with depth at most n (this is inductive) and then whatever you want to do with this type can maybe be shown to only need finite depth.

[awalterschulze]

The Agda version also tries to get around some other termination issues using a sized type, like so

i : Size
record Lang i (P : ◇.Lang) : Set (suc ℓ) where
   coinductive
   field
     ν : Dec (◇.ν P)
     δ : ∀ {j : Size< i} → (a : A) → Lang j (◇.δ P a)

Note Size and Size< are defined as Agda builtins

{-# BUILTIN SIZE     Size     #-}
{-# BUILTIN SIZELT   Size<_   #-}

Is something like this, what you are referring to?

I have started to make an attempt here: https://github.com/katydid/symbolic-automatic-derivatives/blob/sized_automatic/Sadol/SizedAutomatic.lean

I don't know what I am doing, but this is not working:

inductive Lang {i: Nat} {α: Type u} : Language.Lang α -> Type (u+1) where
  | mk
    (null: Decidability.Dec (Calculus.null R))
    (derive: {j: Nat} -> (a: α) -> @Lang j α (Calculus.derive R a))
    : Lang R

It gives the following error:

(kernel) arg #5 of 'SizedAutomatic.Lang.mk' contains a non valid occurrence of the datatypes being declared

Hopefully I am just doing something stupid with how I am defining the depth and there is an easy fix?

[Edward van de Meent]

btw, it might be helpful if you were to post a #mwe . (things like Calculus.null throw errors in a plain project)

[awalterschulze]

Is Calculus.null not working for you? What error is it throwing?

[Edward van de Meent]

things like unknown identifier 'Calculus.derive'.

[Edward van de Meent]

basically, it would be helpful if you could abstract your issue so it would work in the live-lean context. (in case you didn't know about this, when you post a code block on zulip, in the top right of the block there is a an icon linking to an in-browser lean editor)

[awalterschulze]

Ah you mean if you do not copy the whole project from github. I think it is better to get the whole project from github (in this case). It is as small and has no dependencies. https://github.com/katydid/symbolic-automatic-derivatives

But here is a mwe for convenience:

def Lang (α : Type u) : Type (u + 1) :=
  List α -> Type u

def null {α: Type u} {β: Type v} (f: List α -> β): β :=
  f []

def derives {α: Type u} {β: Type v} (f: List α -> β) (u: List α): (List α -> β) :=
  λ v => f (u ++ v)

def derive {α: Type u} {β: Type v} (f: List α -> β) (a: α): (List α -> β) :=
  derives f [a]

class inductive Dec (P: Type u): Type u where
  | yes: P -> Dec P
  | no: (P -> PEmpty.{u + 1}) -> Dec P

inductive AutoLang {α: Type u} : Lang α -> Type (u+1) where
  | mk
    (null: Dec (null R))
    (derive: (a: α) -> AutoLang (derive R a))
    : AutoLang R

def dec_empty : Dec PEmpty := Dec.no (by intro; contradiction)

def emptyset : Lang α := fun _ => PEmpty

def auto_emptyset {α: Type u}: AutoLang (@emptyset.{u} α) := AutoLang.mk
  (null := dec_empty)
  (derive := fun _ => auto_emptyset)

This gives the following error:

fail to show termination for
  auto_emptyset
with errors
failed to infer structural recursion:
Not considering parameter α of auto_emptyset:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, 'auto_emptyset' does not take any (non-fixed) arguments

[Jannis Limperg]

awalterschulze said:

The Agda version also tries to get around some other termination issues using a sized type, like so

i : Size
record Lang i (P : ◇.Lang) : Set (suc ℓ) where
   coinductive
   field
     ν : Dec (◇.ν P)
     δ : ∀ {j : Size< i} → (a : A) → Lang j (◇.δ P a)

Is something like this, what you are referring to?

Sized types are sort of conceptually related to the fuel approach, but are really a different thing. The Agda implementation is also pretty obviously inconsistent. Let me try to get the fuel approach to work...

[Jannis Limperg]

Here's a type that encodes AutoLang trees which end at some given depth with a stop constructor:

def Lang (α : Type u) : Type (u + 1) :=
  List α -> Type u

def null {α: Type u} {β: Type v} (f: List α -> β): β :=
  f []

def derives {α: Type u} {β: Type v} (f: List α -> β) (u: List α): (List α -> β) :=
  λ v => f (u ++ v)

def derive {α: Type u} {β: Type v} (f: List α -> β) (a: α): (List α -> β) :=
  derives f [a]

class inductive Dec (P: Type u): Type u where
  | yes: P -> Dec P
  | no: (P -> PEmpty.{u + 1}) -> Dec P

def emptyset (α : Type u) : Lang α := fun _ => PEmpty

inductive AutoLang {α: Type u} : Nat → Lang α -> Type (u+1) where
  | stop : AutoLang 0 L
  | mk
    (null : Dec (null R))
    (derive: (a: α) -> AutoLang i (derive R a)) :
    AutoLang (i + 1) R

def dec_empty : Dec PEmpty := Dec.no (by intro; contradiction)

def auto_emptyset {α: Type u} : (i : Nat) → AutoLang i (emptyset α)
  | 0 => .stop
  | i + 1 => .mk dec_empty fun _ => auto_emptyset i

Maybe you can do something with this.

[Daniel Weber]

Do you know about QPF?

[Yuri]

Edward van de Meent said:

how should equality on a coinductive behave?

I am worse than a noob about this, but considering that coinductions, to my knowledge, are 'observations' only, is bisimulation the best that can be done? I don't have further insights, but curious about the same.

[awalterschulze]

The Agda implementation is also pretty obviously inconsistent

@Jannis Limperg obviously?

[awalterschulze]

Yuri de Wit said:

Edward van de Meent said:

how should equality on a coinductive behave?

I am worse than a noob about this, but considering that coinductions, to my knowledge, are 'observations' only, is bisimulation the best that can be done? I don't have further insights, but curious about the same.

Ah yes, I forgot about bisimulation

At a high level a found this paper insightful on bisimulation "Automata and Coinduction (an exercise in coalgebra) - J.J.M.M. Rutten". But that might just be because I love Brzozowski's derivatives too much.

[Andrés Goens]

CC @Alex Keizer

[Yuri]

awalterschulze said:

Automata and Coinduction (an exercise in coalgebra

From the paper (thanks):

Two states that are related by a bisimulation relation are observationally indistinguishable in the sense that 1. they give rise to the same observations, and 2. performing on both states the same experiment will lead to two new states that are indistinguishable again.

And this:
image.png

[Jannis Limperg]

awalterschulze said:

The Agda implementation is also pretty obviously inconsistent

Jannis Limperg obviously?

Here's one issue about it: https://github.com/agda/agda/issues/2820

If you search on the Agda bug tracker for the false label, you'll find a bunch more. By 'obviously inconsistent' I mean that the sized types Agda implements are not just broken because of some bug in the type checker but because the design is wrong. I did my master on this (sort of), but didn't manage to come up with a design that is consistent and also preserves the ergonomics of Agda's design.

[Jannis Limperg]

Imo every paper that uses sized types should include a note about this. It's essentially like using type-in-type.

[awalterschulze]

Jannis Limperg said:

Here's a type that encodes AutoLang trees which end at some given depth with a stop constructor:

def Lang (α : Type u) : Type (u + 1) :=
  List α -> Type u

def null {α: Type u} {β: Type v} (f: List α -> β): β :=
  f []

def derives {α: Type u} {β: Type v} (f: List α -> β) (u: List α): (List α -> β) :=
  λ v => f (u ++ v)

def derive {α: Type u} {β: Type v} (f: List α -> β) (a: α): (List α -> β) :=
  derives f [a]

class inductive Dec (P: Type u): Type u where
  | yes: P -> Dec P
  | no: (P -> PEmpty.{u + 1}) -> Dec P

def emptyset (α : Type u) : Lang α := fun _ => PEmpty

inductive AutoLang {α: Type u} : Nat → Lang α -> Type (u+1) where
  | stop : AutoLang 0 L
  | mk
    (null : Dec (null R))
    (derive: (a: α) -> AutoLang i (derive R a)) :
    AutoLang (i + 1) R

def dec_empty : Dec PEmpty := Dec.no (by intro; contradiction)

def auto_emptyset {α: Type u} : (i : Nat) → AutoLang i (emptyset α)
  | 0 => .stop
  | i + 1 => .mk dec_empty fun _ => auto_emptyset i

Maybe you can do something with this.

This is almost working, but there might be an issue with binary operators like or

def get_null {_hi: i > 0} (l: AutoLang i R): Dec (null R) :=
  match l with
  | .mk n _ => n

def get_derive {α: Type u} {R: Lang α} (l: AutoLang (i + 1) R) (a: α): AutoLang i (derive R a) :=
  match l with
  | .mk _ d => d a

def lang_or {α: Type u} (P : Lang α) (Q : Lang α) : Lang α :=
  fun w => P w ⊕ Q w

def sum {α β: Type u} (a: Dec α) (b: Dec β): Dec (α ⊕ β) :=
  match (a, b) with
  | (Dec.no a, Dec.no b) =>
    Dec.no (fun ab =>
      match ab with
      | Sum.inl sa => a sa
      | Sum.inr sb => b sb
    )
  | (Dec.yes a, Dec.no _) =>
    Dec.yes (Sum.inl a)
  | (_, Dec.yes b) =>
    Dec.yes (Sum.inr b)

theorem hi: ∀ (i: Nat), i + 1 > 0 := by
  simp

def auto_or {α: Type u} {P Q: Lang α} (i: Nat) (p: AutoLang i P) (q: AutoLang i Q): AutoLang i (lang_or P Q) :=
  match i with
  | 0 => .stop
  | i' + 1 =>
    .mk
      (null := sum (@get_null _ _ _ (hi i') p) (@get_null _ _ _ (hi i') q))
      (derive := fun (a: α) => auto_or i' (get_derive p a) (get_derive q a))

Here it is only reproduced with one size, but I assume I would actually need two sizes i and j
But I am double checking this now

[awalterschulze]

Yeah this becomes an issue with concat, which when it derives it requires two levels. But this is not a small example and would be easier to check out the repo for.

I have made as much progress as I can on the sized_automatic2 branch: https://github.com/katydid/symbolic-automatic-derivatives/tree/sized_automatic2

[awalterschulze]

Here's one issue about it: https://github.com/agda/agda/issues/2820

If you search on the Agda bug tracker for the false label, you'll find a bunch more. By 'obviously inconsistent' I mean that the sized types Agda implements are not just broken because of some bug in the type checker but because the design is wrong. I did my master on this (sort of), but didn't manage to come up with a design that is consistent and also preserves the ergonomics of Agda's design.

Thanks this is good to know and I added a note to the readme about this

[awalterschulze]

Probably easier to look at files in the pull request review, so I made a broken pull request https://github.com/katydid/symbolic-automatic-derivatives/pull/3/files

[Yuri]

Sorry for intruding on your thread @awalterschulze , but I want to leave this here:

Total Functional Programming by D.A. Turner

It places codata in context, which was wonderful for my own superficial understanding.

[Alex Keizer]

awalterschulze said:

Jannis Limperg said:

Here's a type that encodes AutoLang trees which end at some given depth with a stop constructor:

def Lang (α : Type u) : Type (u + 1) :=
  List α -> Type u

def null {α: Type u} {β: Type v} (f: List α -> β): β :=
  f []

def derives {α: Type u} {β: Type v} (f: List α -> β) (u: List α): (List α -> β) :=
  λ v => f (u ++ v)

def derive {α: Type u} {β: Type v} (f: List α -> β) (a: α): (List α -> β) :=
  derives f [a]

class inductive Dec (P: Type u): Type u where
  | yes: P -> Dec P
  | no: (P -> PEmpty.{u + 1}) -> Dec P

def emptyset (α : Type u) : Lang α := fun _ => PEmpty

inductive AutoLang {α: Type u} : Nat → Lang α -> Type (u+1) where
  | stop : AutoLang 0 L
  | mk
    (null : Dec (null R))
    (derive: (a: α) -> AutoLang i (derive R a)) :
    AutoLang (i + 1) R

def dec_empty : Dec PEmpty := Dec.no (by intro; contradiction)

def auto_emptyset {α: Type u} : (i : Nat) → AutoLang i (emptyset α)
  | 0 => .stop
  | i + 1 => .mk dec_empty fun _ => auto_emptyset i

Maybe you can do something with this.

This is almost working, but there might be an issue with binary operators like or

def get_null {_hi: i > 0} (l: AutoLang i R): Dec (null R) :=
  match l with
  | .mk n _ => n

def get_derive {α: Type u} {R: Lang α} (l: AutoLang (i + 1) R) (a: α): AutoLang i (derive R a) :=
  match l with
  | .mk _ d => d a

def lang_or {α: Type u} (P : Lang α) (Q : Lang α) : Lang α :=
  fun w => P w ⊕ Q w

def sum {α β: Type u} (a: Dec α) (b: Dec β): Dec (α ⊕ β) :=
  match (a, b) with
  | (Dec.no a, Dec.no b) =>
    Dec.no (fun ab =>
      match ab with
      | Sum.inl sa => a sa
      | Sum.inr sb => b sb
    )
  | (Dec.yes a, Dec.no _) =>
    Dec.yes (Sum.inl a)
  | (_, Dec.yes b) =>
    Dec.yes (Sum.inr b)

theorem hi: ∀ (i: Nat), i + 1 > 0 := by
  simp

def auto_or {α: Type u} {P Q: Lang α} (i: Nat) (p: AutoLang i P) (q: AutoLang i Q): AutoLang i (lang_or P Q) :=
  match i with
  | 0 => .stop
  | i' + 1 =>
    .mk
      (null := sum (@get_null _ _ _ (hi i') p) (@get_null _ _ _ (hi i') q))
      (derive := fun (a: α) => auto_or i' (get_derive p a) (get_derive q a))

Here it is only reproduced with one size, but I assume I would actually need two sizes i and j
But I am double checking this now

This kind of construction is exactly what QpfTypes generates. The library is a bit rough still, but using it should be easier than doing the whole construction by hand. (And if it's not, please do tell me what you run into, so I can fix that)

[awalterschulze]

I look at the library, but I don't know if it will work with this indexed type

[Alex Keizer]

Ah, sorry, I missed that your type has an index. The library indeed does not support that yet