<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Hi.<br>
    <br>
    Sorry but I don't really understand Andrej and Mathieu's last mails.
    In size-based termination, there is no ordinal in the type system
    itself. Ordinals are just used in the meta-theory to justify that,
    indeed, every well typed term terminates. In fact, ordinals were
    already used before in the meta-theory of CIC (see Altenkirch and
    Werner's PhDs) to justify the fact that functions defined by
    structural induction indeed terminates. Size-based termination
    simply extends the syntax of CIC by making explicit something that
    was implicit in the interpretation of types as Girard's reducibility
    candidates. The nice thing is that it brings extra power to prove
    the termination of functions because, in contrast to the notion of
    "structurally smaller", size is invariant by reduction.<br>
    <br>
    Best regards,<br>
    <br>
    Fr&eacute;d&eacute;ric.<br>
    <br>
    <div class="moz-cite-prefix">Le 09/01/2014 00:25, Matthieu Sozeau a
      &eacute;crit&nbsp;:<br>
    </div>
    <blockquote
cite="mid:CALgtc7h_JF1T4zpAZQA4=2RrsNSwA24oSvp97ZMay8633Hu+6Q@mail.gmail.com"
      type="cite">I agree with you Andrej, and the (well founded)
      transitive closure of the&nbsp;subterm relation can easily be defined
      for computational inductive families&nbsp;(all inductive types if you
      remove prop), avoiding the&nbsp;computation&nbsp;of&nbsp;ordinals. That's
      precisely the "semantic" (maybe&nbsp;"evidence-based"?)&nbsp;explanation
      that C. Paulin&nbsp;used in her habilitation thesis to justify
      recursive definitions and the most general one for users (it does
      not even need to be attached to an inductive type). Equations can
      derive this subterm relation automatically for (non-mutual,
      non-nested) inductive families, and prove its wellfoundedness.
      Extending this to the other cases is a matter of thinking and
      engineering.&nbsp;The Below predicate of Epigram gives you
      similar&nbsp;access to every subterm you can recurse on
      "logically".&nbsp;The only culprit is&nbsp;reduction behavior/efficiency
      using this machinery, but that should be optimizable.<span></span>
      <div>
        <div><br>
        </div>
        <div>Best,<br>
          <div>-- Matthieu<br>
            <br>
            Le mercredi 8 janvier 2014, Andrej Bauer a &eacute;crit&nbsp;:<br>
            <blockquote class="gmail_quote" style="margin:0 0 0
              .8ex;border-left:1px #ccc solid;padding-left:1ex">I would
              just like to point out that ordinals are an inherently<br>
              classical notion. The correct constructive and
              computationally<br>
              meaningful replacement is that of a well-founded relation,
              i.e., a<br>
              relation &lt; on a set X satisfying, for all properties P,<br>
              <br>
              &nbsp;(forall y, ((forall x &lt; y, P x) -&gt; P y)) -&gt;
              forall z, P z.<br>
              <br>
              This is all well known, and of course you can recognize
              the<br>
              recursor/eliminator in the above formula. So if we are to
              take<br>
              computation seriously, we ought to think about inductive
              definitions<br>
              which are justified by a more general notion of well
              foundedness, not<br>
              just ordinals. The ordinals are bound to go wrong when we
              push them a<br>
              little bit.<br>
              <br>
              Also, the HoTT experience has thought us (at least me) the
              value of<br>
              semantic notions over syntactic ones. I am referring to
              HoTT hProp vs.<br>
              CiC Prop. The former delineates the concept of
              "proposition" with a<br>
              semantic condition, while the latter does it
              formalistically. It would<br>
              seem sensible to me to go the same route with inductive
              definitions,<br>
              namely, rely on semantic justifications rather than
              syntactic ones. [I<br>
              may be misusing the words "semantic" and "syntactic" here,
              but I<br>
              cannot think of better ones.]<br>
              <br>
              With kind regards,<br>
              <br>
              Andrej<br>
              <br>
              --<br>
              You received this message because you are subscribed to
              the Google Groups "Homotopy Type Theory" group.<br>
              To unsubscribe from this group and stop receiving emails
              from it, send an email to <a moz-do-not-send="true"
                href="javascript:;" onclick="_e(event, 'cvml',
                'HomotopyTypeTheory+unsubscribe@googlegroups.com')">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br>
              For more options, visit <a moz-do-not-send="true"
                href="https://groups.google.com/groups/opt_out"
                target="_blank">https://groups.google.com/groups/opt_out</a>.<br>
            </blockquote>
          </div>
        </div>
      </div>
      <br>
      <br>
      -- <br>
      -- Matthieu<br>
      -- <br>
      You received this message because you are subscribed to the Google
      Groups "Homotopy Type Theory" group.<br>
      To unsubscribe from this group and stop receiving emails from it,
      send an email to <a class="moz-txt-link-abbreviated" href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br>
      For more options, visit <a moz-do-not-send="true"
        href="https://groups.google.com/groups/opt_out">https://groups.google.com/groups/opt_out</a>.<br>
    </blockquote>
    <br>
  </body>
</html>