[POPLmark] How to believe the Twelf proof of 1a

[Frank Pfenning]

Hi Randy,

Virga calls it dependence relation, which was a bit unfortunate due to
the clash with "dependent types" so we went back to the earlier term of
"subordination".  See Definition 2.1.3 and the discussion later in
section 2.1.  There is also a summary of it on page 10 of
<http://www.cs.cmu.edu/~fp/papers/esop96.pdf> and its use in termination
checking.  It is probably also reviewed in Carsten's thesis.

It accomplishes the following.  In a framework such as Coq where
you make explicit inductive definitions, all the constructors for
a type must come together, and they can depend on any type declared
before and none declared after.  In an open-ended framework such
as LF, no such discipline exists.  However, the meta-logic
must take advantage of this information occasionally.  For example,
cut elimination for first-order logic is terminating because

[t/x]A is strictly smaller than forall x.A

but that is only true if no formula A can appear inside the term t.
Subordination tracks this by saying that "term" is subordinate to
"formula" but not vice versa.  You can display the subordination
relation in Twelf by using Twelf.Print.subord (); or Print.subord

  - Frank

> Karl Crary writes:
>  > The precise statement you want to check is that var is not subordinate 
>  > to sub.
>  > 
>  > The notion of subordination is formalized in Roberto Virga's thesis.
>  > [...]
> 
> According to acroread, the literal string "subord" does not occur in
> Roberto Virga's thesis (CMU-CS-99-167).
> 
> Randy