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?
