Talk:Output freeness

From The Twelf Project

This topic was on the other wiki as well: http://fp.logosphere.cs.cmu.edu/twelf/?n=Answers.Freeness . It's by Geoff Washburn, not me, so if you include a lot from that file you'll need to add a {{license-by-sa}} tag. — Rob (and his talk) 16:57, 7 September 2006 (MST)

• Oops, I didn't notice that. Well, my MIT-license version seems to have all the same info, so I don't think there's any need to import it, though perhaps the example could be a little simpler.  — Tom 7 06:54, 11 September 2006 (MST)

[edit] How does output coverage differ from output freeness?

That question deserves a thorough answer, but Jason and I came up with this program while screwing around: observe that fake-thm output covers, even though the subgoal invocation of ff in the ft/z case is not "output free" because the output argument is a ground term:

nat : type.
s : nat -> nat.
z : nat.

bool : type.
t : bool.
f : bool.

add : nat -> nat -> nat -> type.
%mode add +M +N -O.

add/z : add M z M.
add/s : add M (s N) (s O')
     <- add M N O'.

%worlds () (add _ _ _).
%total N (add _ N _).

boolcont : bool -> type.
@ : {B} boolcont B.

ff : {B : bool} {C : boolcont B} type.
%mode ff +B -C.
- : ff B (@ B).

fake-thm : {M : nat} type.
%mode fake-thm -N.

ft/z : fake-thm z
 <- ff t (@ t).

%worlds () (ff _ _) (fake-thm _).
%total D (ff D _).
%total [] (fake-thm _).

 — Tom 7 16:58, 26 October 2006 (EDT)