<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édéric.<br>
<br>
<div class="moz-cite-prefix">Le 09/01/2014 00:25, Matthieu Sozeau a
écrit :<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 subterm relation can easily be defined
for computational inductive families (all inductive types if you
remove prop), avoiding the computation of ordinals. That's
precisely the "semantic" (maybe "evidence-based"?) explanation
that C. Paulin 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. The Below predicate of Epigram gives you
similar access to every subterm you can recurse on
"logically". The only culprit is 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 écrit :<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 < on a set X satisfying, for all properties P,<br>
<br>
(forall y, ((forall x < y, P x) -> P y)) ->
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>