7
$\begingroup$

In Agda we can prove termination of functions by using well-founded relations, is there a guideline for proving datatype declarations strictly positive, possibly via use of some container techniques together with well-founded relations?

I have been trying to port Danielsson's A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family to modern Agda and there I have encountered the following argument.

Rendered in more modern Agda:

-- Values

  -- This data type is a little problematic, since Val occurs
  -- negatively in ΠVal and ΠValCong. However, notice that the spines
  -- of the types of the recursive components are decreasing in
  -- ΠVal/ΠValCong, and non-increasing in all other constructors. This
  -- should ensure that the type is well-founded. I'm not aware of any
  -- meta-theory explaining a type such as Val, though.
mutual
    {-# NO_POSITIVITY_CHECK #-}
    data Val : {Γ : Ctxt} {τ : Ty Γ} -> (Γ ⊢ τ) -> Set where
        ✶Val : {Γ : _} {x : Γ ⊢ ✶ Γ } -> Atom x -> Val x
        ElVal : {Γ : _} {n : _} {t' : Γ ⊢ U n} {t : Γ ⊢ El t'} -> Atom t -> Val t
        _∷ˢ_ : {Γ¹ : Ctxt} {τ¹ : Ty Γ¹} {t¹ : Γ¹ ⊢ τ¹}
            {Γ² : Ctxt} {τ² : Ty Γ²} {t² : Γ² ⊢ τ²} -> Val t¹
            -> (t¹ ≈⊢ t²) -> Val t²
        ΠVal : {Γ : Ctxt} {τ₁ : Ty Γ} {τ₂ : Ty (Γ ▻ τ₁)} {t₁ : Γ ⊢ Π τ₁ τ₂}
          -> ΠFun t₁ -> Val t₁
    ΠFun : {Γ : Ctxt} {τ₁ : Ty Γ} {τ₂ : Ty (Γ ▻ τ₁)}
      -> (t₁ : Γ ⊢ Π τ₁ τ₂) -> Set
    ΠFun {Γ = Γ} {τ₁ = τ₁} t₁ = (Γ' : RCtxt Γ)
      -> (t₂ : (Γ ++ Γ') ⊢ (τ₁ / wk⋆ Γ'))
      -> (v₂ : Val t₂)
      -> Val (app (t₁ /⊢ wk⋆ _) t₂)

Are there any techniques that could allow formalizing this argument? Note that it is possible to unroll $\Pi$Fun, the induction-recursion here is not essential.

$\endgroup$
5
  • $\begingroup$ I'm afk now, but some quick conments: 1) You can use variable declaration to save lots of implicit variables. Also, ∀ {x y} is equivalent to {x : _} {y : _}. 2) Maybe you shouldn't use lists and _++_. Use binary trees where _++_ is a constructor instead. $\endgroup$
    – Trebor
    Sep 28, 2022 at 4:55
  • $\begingroup$ Also, can you reformulate Val as a recursive type instead? That is typically the solution given your comments. $\endgroup$
    – Trebor
    Sep 28, 2022 at 5:01
  • 1
    $\begingroup$ You may want to ask your question on the Agda mailing list where you're more likely to get an answer from NAD himself. $\endgroup$
    – gallais
    Sep 28, 2022 at 7:57
  • $\begingroup$ @Trebor I cannot reformulate it using a recurisve type due to the cast constructor ∷ˢ, i can try encoding it recursively but then each case also includes the tricky cast constructor and ≈⊢, this would go away if we could encode that quotient type, but that is a chicken-and-egg problem as this construction is used in proof of normalization about ≈⊢ as a judgmental equality, and type theory without quotients seems to need normalization already to define it, see definable quotients by Altenkirch et al. $\endgroup$
    – Ilk
    Sep 29, 2022 at 0:33
  • $\begingroup$ Check out whether you can encode your data type using Guarded (Cubical) Agda and perhaps wait until github.com/agda/agda/issues/6587 is fixed $\endgroup$ Jun 9, 2023 at 13:43

2 Answers 2

3
$\begingroup$

Are there any techniques that could allow formalizing this argument?

Beluga has a notion of 'stratified types' that corresponds to this type of construction. From the user manual:

We distinguish between inductive types and stratified types. Inductive types correspond to fix-point definitions in logic and must be strictly positive, i.e. the type family we are defining cannot occur in a negative occurrence. Stratified types define a recursive type by induction on an index argument. As a consequence, the type family we are defining may occur in a negative position, but the index is decreasing.

I don't know however if the current system would be able to detect that the type of values ought to be accepted.

$\endgroup$
2
  • $\begingroup$ Is this the same concept as recursive types (maybe ind-rec types), or subtly different? $\endgroup$
    – Trebor
    Sep 28, 2022 at 12:03
  • $\begingroup$ This seems like almost the solution, I am left to wonder. Can these be encoded using other constructions in i.e. agda with IR? but these seem like almost the right construction, have to dive a bit into it. $\endgroup$
    – Ilk
    Sep 29, 2022 at 0:31
1
$\begingroup$

Here's a solution, that I have been making progress with, that fits normal Agda.

The aim of defining a type via induction, yet allowing non-obviously decreasing argument in a negative position can be approached via levitation from The Gentle Art of Levitation. The trick there is to introduce a syntax and interpretation of indexed datatypes.

The syntax is

data IDesc (I : Set) : Set₁ where
  var : (i : I) -> _
  k : (A : Set) -> _
  _×D_ : (D1 : IDesc I) -> (D2 : IDesc I) -> _
  ΣD ΠD : (S : Set) -> (T : S -> IDesc I) -> _

We also need an interpretation function [|_|] : {I : Set} -> IDesc I -> (P : I -> Set) -> Set, that interprets variables by P and other constructors by the obvious recursion, i.e. k by its argument, ΣD - by
Σ S (λ s → [| T s |] P), etc.

and then we have a least fixpoint on IDesc

data IMu {I : Set} (R : I -> IDesc I) (i : I) : Set where
  con : [| (R i) |] (λ j → IMu R j) -> IMu R i

Note that the troubling call becomes the first argument to ΠD after inlining and translating into the syntax of IDesc.

we thus define the type as

Vallev : (Σ _ λ Γ → Σ _ λ τ → Γ ⊢ τ) -> Set
Vallev x = IMu (λ (a , b , c) → ValDesc c) x

and ValDesc as

 ΣD ValCon ...

where ValCon is

data ValCon : Set where
  valstar : _
  valel : _
  valcons : _
  valpi : _

Here we will focus only on the problematic valpi case. The trouble here is that ΠD takes first argument a Set not a description. We thus need to apply ΠD to the result of applying IMu to the whole description. This is where the failure of strict positivity comes from.

We can now define a single function

data MutualLevDesc : Set where
  Lev : MutualLevDesc
  Desc : MutualLevDesc

DescType =  {Γ : Ctxt} -> {τ : Ty Γ} -> (t : Γ ⊢ τ) -> IDesc (Σ Ctxt (λ Γ → Σ (Ty Γ) λ τ → Γ ⊢ τ))
LevType = (Σ _ λ Γ → Σ _ λ τ → Γ ⊢ τ) -> Set
ValLevDesc : (m : MutualLevDesc) -> case m of λ{Lev → LevType
                                            ; Desc → DescType}
ValLevDesc = ...

and voila strict positivity becomes a termination proof for this function, ValLevDesc, we now have hope that we can use standard techniques of well-founded recursion to prove this function terminating.

Our original datatype would then be

Val = ValLevDesc Lev
$\endgroup$
1
  • 1
    $\begingroup$ This is a pretty nice result if you can make it work out, as the motivation for that line of work is to bring more of the actual programming machinery in type theory to bear on data type definitions. If it's just naturally flexible enough to define something that doesn't fit into the traditional, rigid specifications, that's a significant benefit. $\endgroup$
    – Dan Doel
    Oct 1, 2022 at 4:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.