Error in spanning tree algorithm?

[davidweichiang]

The paper says to construct a graph where if de/refunctionalizing type t1 changes it to a type containing t2, then draw an edge from t1 to t2. But what if t1 de/refunctionalizes into (t2->t3) where t2 and t3 are both recursive? Moreover, what if t2 de/refunctionalizes to t1? This would have a spanning tree even though de/refunctionalization will fail.

[davidweichiang]

Unfortunately it seems like we might have to find the minimum spanning tree of a hypergraph, which is NP-complete.

[davidweichiang]

Hm, I thought this program would illustrate the problem, but it appears your code does something smarter and correctly fails:

data Nat = zero | succ Nat;
data Nat' = zero' | succ' Nat';
data Nat'' = zero'' | succ'' Nat'';
data Unit = unit;

define prime : Nat -> Nat' = \n: Nat.
  case n of
    | zero -> zero'
    | succ m -> succ' (prime m);

define unprime : Nat' * Nat'' -> Nat = \p: Nat' * Nat''.
  let (n', n'') = p in
    case n' of
      | zero' -> zero
      | succ' m' -> succ (unprime (m', n''));

define gen'' : Unit -> Nat'' = \u: Unit. zero'';

unit

[davidweichiang]

OK, I see, you're using a greedy algorithm for finding a spanning tree of a hypergraph. Is it the fact that it's not a minimum spanning tree that a greedy algorithm works? We'll need to add a proof of that, I think. I'll start by changing what's written to what's actually implemented correctly (not for the first time).