5
$\begingroup$

A "very dependent function" is a function whose output type at input $n$ depends on its own output values at inputs $k<n$. Is there a precise definition of such things that makes sense in formal dependent type theory (e.g. Martin-Lof Type Theory or the Calculus of Constructions)?

The reference everyone points to for very dependent functions is Hickey's Formal Objects in Type Theory Using Very Dependent Types (section 3). But it looks to me like he only gives a PER-style semantics, not a syntax that stands on its own. In particular, his definition might be implementable in a NuPRL-like proof assistant (maybe --- I don't know enough about such proof assistants to be sure), but it's not clear to me how it could be implemented in a proof assistant like Agda, Coq, or Lean. Is my reading of Hickey correct? Has anyone ever implemented very dependent functions in a proof assistant based on something like MLTT or CoC?

$\endgroup$
10
  • $\begingroup$ Related: github.com/UlfNorell/insane $\endgroup$
    – ice1000
    Sep 14 at 23:32
  • $\begingroup$ Did you ask this because OHTT seems to need this? $\endgroup$
    – ice1000
    Sep 14 at 23:40
  • $\begingroup$ @ice1000 Why would you think that? $\endgroup$ Sep 15 at 14:45
  • $\begingroup$ for reasons that are off-topic on this website. Basically, in recent days, whenever/wherever I see you, I start to think about OHTT. I also overgeneralized the fact that you've opened a lot of Agda issues that are related to OHTT formalization to "everything Mike Shulman do has something to do with OHTT". Hence the above comment. $\endgroup$
    – ice1000
    Sep 15 at 22:31
  • $\begingroup$ Well, I do seem to be spending a lot of time on H.O.T.T. these days, but I do still have other interests too. (-: $\endgroup$ Sep 16 at 2:17

1 Answer 1

1
$\begingroup$

It looks like the rules in Table 1 of Hickey's Formal Objects in Type Theory Using Very Dependent Types (section 3) as cited in the question are syntactic in nature and can be implemented immediately in a tactic-and-realizability-based type theory with refinement types. The rules as written would make typing of terms undecidable even with a separate syntactic form for very-dependent lambdas since it would be necessary to invent a well-founded order for each type and term formation. They would also be rather horrible to write out in full thanks to the $WellFounded_i$ predicate.

To adapt them to actual practical implementation in an intensional type theory, what I think I would do is rely on the structural order. That is, the formation rule for the type $\lbrace f | x : A \to B \rbrace$ would allow multiple arguments inside the braces, but only allow $f$ to be called in a structurally decreasing way just as in structural termination checking. This is much more amenable to syntactic checking and the full power of very dependent types could be recovered via accessibility predicates as in the usual library-based implementation of well-founded recursion. Something like: $$ \frac{\Gamma, \Delta, f : \lbrace f\ |\ \Delta \to B\rbrace \vdash B\ \mathrm{type}\ \text{($B$ structurally decreasing in $\Delta$)}}{\Gamma \vdash \lbrace f\ |\ \Delta \to B\rbrace\ \mathrm{type}} \text{$\lbrace\rbrace$-form} \\ \ \\ \frac{\Gamma \vdash \lbrace f\ |\ \Delta \to B\rbrace\ \mathrm{type} \\ \Gamma, \Delta \vdash B[t/f]\ \mathrm{type} \\ \Gamma, \Delta \vdash t : B[t/f] }{\Gamma \vdash\rho\ \Delta \to t : \lbrace f\ |\ \Delta \to B\rbrace} \text{$\lbrace\rbrace$-intro} \\ \ \\ \frac{\Gamma \vdash \lbrace f\ |\ \overline{x_i : A_i} \to B\rbrace\ \mathrm{type} \\ \overline{\Gamma \vdash t_i : A_i[\overline{t_{j<i}/x_{j<i}}]} \\ \Gamma \vdash u : \lbrace f\ |\ \overline{x_i : A_i} \to B\rbrace \\ \Gamma \vdash B[u/f,\overline{t_i/x_i}]\ \mathrm{type}}{\Gamma \vdash u.[\overline{t_i}] : B[u/f,\overline{t_i/x_i}]} \text{$\lbrace\rbrace$-elim} \\ $$ (for now I've elided the rules for $\beta$, type equality and value equality).

I think https://github.com/UlfNorell/insane implements something similar to this but without the structural recursion restriction, so unsafe.

$\endgroup$
2
  • $\begingroup$ The conclusion of {}-form seems to have an extraneous "$f :$" in the conclusion, and something is wrong with the context in the conclusion of {}-intro. $\endgroup$ Sep 21 at 8:50
  • $\begingroup$ @AndrejBauer Edited, thanks. $\endgroup$ Sep 21 at 11:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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