April 28th, 2007

beartato phd

(no subject)

Found an alarming counterexample to my expectations about the termination of higher-order unification. I hope I'm just being really stupid here and missing something obvious.

Collapse )

Below is some twelf code that illustrates the problem, with a %query not terminating, despite a %terminates check. I feel like I should be able to twist this into a simple type-checking problem, but my brain hasn't coughed it up yet.

Collapse )

Another update: Frank's reply to my twelf-bearing email contains the word "Oops", so I guess I have found a real bug in the implementation and am not discovering known problems. I've mixed feelings: finding bugs is good, but bugs being there to be found is bad.
beartato phd

(no subject)

Aha, found a fine little idiom for getting arbitrary unification equations to arise from twelf's type reconstruction algorithm. I don't know why I never had to figure this out before. Should probably toss it on the wiki at some point.

Anyway, using it, I can write the following signature, which causes twelf to go into an infinite loop. I'm basically certain it's in unification, not the later abstraction phase where a known termination bug was located.
o : type.
f : o -> o.
eq : (o -> o -> o) -> (o -> o -> o) -> type.
refl : eq M M.
c :     eq ([a] [b] X a) ([a] [b] f (Y (Z b)))
     -> eq ([a] [b] Y a) ([a] [b] X (Z b))
     -> type. 
test : c refl refl.
beartato phd

(no subject)

n1h2k played at the so-called "roboprom" tonight, some sort of dress-up sit-down wine-and-dine thing for the robotics students. It didn't beat Ruy's party for musical togetherness or rewarding insanity of people in attendance, but I still had a lot of fun. It was nice to be able to be significantly less well dressed (I for instance had on like a tie and corduroy jacket, and jeans and sneakers) than everyone else (who were wearing decent suits) and not care, because we were the band. Pretty fucking exhausted now though.