This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype.

The idea (rephrased):
If the argument to a datatype decreases in a well-founded way in non-strictly positive positions, and is non-increasing in all other inductive positions, the datatype should exist.

What I thought I would do:
Extend the codes of descriptions with Sigma/Pi/var/constants, with a requirement on var to be non-increasing in the measure and Pi having an encoded decrease.

The trouble:
Trying to take a least fixed point of a datatype where occurrences decrease in non-strictly positive positions and are non-increasing in all other positions. Here I reproduce only the parts of definitions that trigger the positivity check. Seemingly the solution: To the following datatype of indexed descriptions:

data IDesc {l : Level}(I : Set l) : Set (lsuc l) where
  var : I -> IDesc I
  const : Set l -> IDesc I
  prod sum : IDesc I -> IDesc I -> IDesc I
  sigma pi : (S : Set l) -> (S -> IDesc I) -> IDesc I

with a decoding function

decode : {l : Level}{I : Set l}
  -> IDesc I -> (I -> Set l) -> Set l
decode (var x) r = r x
decode (const x) r = x
decode (prod x y) r = decode x r × decode y r
decode (sum x y) r = decode x r ⊎ decode y r
decode (sigma S x) r = Σ S λ s → decode (x s) r
decode (pi S x) r = (s : S) → decode (x s) r

and a least fixpoint

data μ {l : _} {I : Set l}
   {measure : I -> I -> Set l} (wfm : WellFounded measure) 
   (D : IDesc wfm) (o : I -> Set l) (i : I) : Set l where
  inμ : descT {_} {_} {_} wfm D (μ wfm D o) i -> _

we add the following arguments

{measure : I -> I -> Set l}(wfm : WellFounded measure)

representing that occurrence is decreasing, resp. non-increasing in a well-founded way. And modify var in the following way.

descT {measure = m} wfm (var x) r o = (x ≡ o ⊎ m x o) × r x

To represent that a pi where argument decreases we use the following, note this makes the Desc and descT inductive-recursive. This was something I tried, I do not believe it is correct, but I would like to understand what is going wrong in the positivity check here.

pi : ∀{i}{w} (f : descT wfm w (λ z → measure z i) i -> IDescT wfm) -> IDescT wfm

with decoding function

descT wfm (pi f) r o = ∀ y -> descT wfm (f y) r o

Now Agda sees that positivity check fails for $ \mu $, but most importantly removing $ \times \: r \: x$ from the var case make construction of $\mu$ succeed and as expected so does just removing pi. What makes Agda's strict positivity check fail here? What is the primitive type that we are trying to construct here and what fails?

I understand that Agda can not see through the non-increasing/decrease argument, but what is causing the interaction between the 2 clauses? Is there an explanation for some kind of pairwise condition on IR clauses that Agda uses to see that the least fixed point exists? Is there some direct way, such as trying to construct a container of the IR that could let me bypass the strict positivity check here by proving more semantic conditions?

  • $\begingroup$ I think the most reliable source is the source code of Agda itself.. and the second most reliable one is those who wrote that code :) $\endgroup$
    – Trebor
    Commented Oct 30, 2022 at 7:56
  • $\begingroup$ Feel free to create a tag wiki for induction-recursion (or well-founded-induction) $\endgroup$
    – Couchy
    Commented Oct 30, 2022 at 18:20


Your Answer

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