2 questions about Twelf

[gusl]

If I want to assert that a function could be specified either as a -> b -> c or b -> a -> c, I would like to write it as (a * b) -> c, or some similar notation. Is this supported?

Can one declare in Twelf that a function is commutative? i.e., if f takes two arguments of the same type, I'd like to declare that for all a,b, f(a,b) is equal to f(b,a). Is this possible? While one can imagine doing static analysis, I just want to be able to declare it.

Comments

[simrob.livejournal.com]

I'm afraid the answer is "no." The problem from your perspective is that Twelf has a VERY strong notion of what "equals" means - from Twelf's perspective, f(a,b) is equal to f(b,a) iff a and b are equal. Other notions of equivalence can be defined in Twelf, for instance when I define evals : exp -> nat -> type which relates a numerical expression to the natural number it evaluates to, and then I can prove a theorem that, say evals (A + B) N1 and evals (B + A) N2 implies that N1 is equal to N2 (and this is "equals" in the very strong syntactically-equal sense).

[gustavolacerda.livejournal.com]

So you need to actually implement addition in order to prove that it's commutative. This makes sense.

But I don't want to prove it. I just want to declare it.

Is exp "expression"? Is evals a relation? Is it a function? (I'm confused by a function that returns something of type type)

[simrob.livejournal.com]

Don't read
evals : exp -> nat -> type
as a function. Read is as a declaration of a dependent type. A more natural example might be this:
nat: type.
z : nat.
s : nat.

indexed_list : nat -> type.
nil : list z.
cons : item -> list N -> list (s N).

So I'm defining an indexed list, and saying that nil is a list of length zero and cons is a constructor that takes an item and a list of length N and returns a list of length N + 1.

[gustavolacerda.livejournal.com]

Again, I don't want to prove it. That would be too hard. I just want to declare it.

I want to use such properties to prove theorems in the language, and save computation.
When an expression evaluates to f(a,b) - f(b,a), I want to check whether f is commutative, and if it is, the above should evaluate to 0. Lovely laziness.

[simrob.livejournal.com]

Right - Twelf isn't tuned at supporting this kind of declaration. I don't know what you mean by computation, unless you mean human computation on the part of the prover.

[gustavolacerda.livejournal.com]

I was also wondering about the first question: how do you express the fact that it makes sense to curry you function by either passing an instance of type a or an instance of type b?

[simrob.livejournal.com]

Could you restate that more clearly? Twelf's language of constructors doesn't have pairs, following the convention that you just curry EVERYTHING.

Design philosophy of Twelf: if you can do it with a simpler underlying theory and it's shockingly more difficult to use the result, then do it with the simpler underlying theory. Having no pairs in the constructor language simplifies the underlying theory, and it's not really any more annoying to use Twelf as a result.

[simrob.livejournal.com]

Two equivalent ways of saying the above

* Twelf doesn't have "functions," it has "constructors"
* All functions in Twelf are injective

The exception are the constraint domains, but those play badly with the theorem-proving part of Twelf that we all know and love.

[gustavolacerda.livejournal.com]

I like the "all functions in Twelf are injective" view.

Constructors? Wouldn't that mean that f(a,b) does not equal f(a,b)? (i.e. f constructs a new object each time it's called)

[simrob.livejournal.com]

Aah - Twelf's equality is only concerned about structure - think of constructors not as new Object() things but as actual building blocks - If I have two "f" Legos, and I tack on A and B to the left and right sides of one "f" Lego, and then I tack on A and B to the right and left sides of the other "f" Lego, then the two resulting Lego constructions have the same structure iff A and B have the same structure.

[chrisamaphone]

constructors in the functional programming sense, not the OO sense. (think datatype constructors, if you've seen those in haskell or ml... data foo = C1 (int) | C2 | ... the Cis are called "constructors.")

[simrob.livejournal.com]

Aah, yes, if you already know ML/Haskell that is obviously the better analogy, I didn't know what your background in functional programming was.

[gustavolacerda.livejournal.com]

yeah, it sounds like I'm talking about a constraint domain.
I want to have a theorem-prover that *uses* those constraints.

[simrob.livejournal.com]

Right - that theorem prover isn't Twelf, I'm afraid. Other proof assistants do have this ability, to the best of my knowledge - you just hit the thing you think is true with "equality reasoning tactic #3" or something and it tries all of the things you're suggesting in some heuristic way.

[chrisamaphone]

to comment a little further on what rob said, the thing that i coded up for you isn't really indicative of common twelf usage patterns. the way i wrote down the types of your "functions" is generally used to write down syntax (as rob said, not functions, but constructors). if you want to actually define what something "does" on a given input, you define a relation, like rob's

evals : exp -> nat -> type

which can, in one light, be read as saying evals is a relation on exps and nats.

you can sort of specify that you want (and have twelf check) such things to behave as functions by giving them modes, indicating which arguments to the relation are "inputs" and which are "outputs". you can also have it check totality of such a thing. uniqueness of output for a given input is something you have to prove as a theorem.

i'm still not sure any of this actually inhibits you from what you want to do. specifically, i'm curious why you'd want to "declare" commutativity.

[simrob.livejournal.com]

It's actually not an uncommon thing to do in, say, rewriting theory. In Twelf, it is important for us to know that ([x] c x x) d is actually Twelf-identical to c d d, and Twelf's constraint domains do allow the kind of things Gustavo is looking for here.

%use equality/integers.

id : integer -> integer -> type.
id/refl : id X X.

%abbrev _ : id (A + (B + C)) ((C + A) + B) = id/refl.

This is part of why constraint domains don't get along with metatheorems - they add so gosh-darn many equalities to the langauge.

why declare commutativity

[gustavolacerda.livejournal.com]

I'd like to do my math inside Twelf or a similar system.

This is partly for the sake of clarity, partly to help me catch errors, and partly to automate mathematical work (e.g. by using theorem-provers).

Formalizing a domain completely is usually unnecessary work. Therefore, I want to declare high-level axioms, such as the commutativity of multiplication... or even higher level, like the central limit theorem. (The system gives no guarantee that they're true).

Re: why declare commutativity

[simrob.livejournal.com]

Right. Such a thing is not bad, has been tried, but is not Twelf.

Rule of thumb: Twelf is a programming language through-and-through, and so if you're going to expect it to believe f(a,b) = f(b,a) then the absolute least you'll have to do is write a program that explains why on earth that is the case. You can tell it "assume this is true and I'll explain why later/never," but this isn't done elegantly in Twelf and seems, in Twelf at least, to lead to making a lot of the problematic errors that you wanted formalization to avoid in the first place.