Thursday, June 12, 2008

Clumsy existential

This might be a dumb question: I often want to prove something like this:
(∃ v . ev) ⇔ (∃ v ~ v . [[e]] ⇒ v′)
except that the scope doesn't work out: v is only in scope in the first parenthesized proposition, so it can't be referred to in the second one. Of course, it's generally sufficient to prove co-termination and just leave out the relationship between the final values, since that's usually easily derivable. But it's an important part of the intuition behind correctness, so I want the relationship between answers to be in the statement of the theorem.

An awkward way to make this work is to write big clunky conjunctions like:
(e⇓ ⇔ [[e]]⇓) ∧ (∀ v . ev . ∃ v′ ~ v . [[e]] ⇒ v′)
But it would be nice if there were some way to write it more compactly like the first pseudo-proposition I wrote. I like that it reads almost like you'd say in English: "e and [[e]] always get the same answers."

Anyone have any suggestions?

7 comments:

Tony Garnock-Jones said...

Is this similar to the "donkey anaphora" problem referred to in http://languagelog.ldc.upenn.edu/nll/?p=230 ?

There, sentences of the form

"Every farmer who owns a donkey beats it"

cannot be straightforwardly translated into first-order predicate logic because of a similar scope/existential-hoisting problem to your example above.

They link to a paper, by Chris Barker and Chung-chieh Shan, about a new approach to the problem: http://semprag.org/article/view/sp.1.1

Perhaps it can shed some light on your problem.

Sjoerd Visscher said...

This is not really my thing, so I wonder, would this work?

∃ v′ ((∃ v ~ v′ . e ⇒ v) ⇔ (∃ v ~ v′ . [[e]] ⇒ v))

As the proposition is symmetric between e and [[e]], it would be nice if it was syntactically symmetric as well.

Dave Herman said...

Sjoerd-- I'm afraid that's not right. There can't be an outer existential; the proposition is not asserting the existence of anything, it's asserting the interdependence of existence.

Dave Herman said...

Tony-- thanks for the pointer. I did see that LL post, and tried looking at their paper but it's over my head (IANA linguist). But I'll see if Ken Shan has any suggestions.

Sjoerd Visscher said...

Of course, thanks.

Maybe you should just define "answer of" and "the same as" operators and write:

answer of e the same as answer of [[e]]

Felix said...

I'm not sure if my interpretation of your first pseudo-proposition matches your own; I think the interpretation depends on whether you are allowing for a non-deterministic semantics. (That is, my intuition about what the first psuedo-proposition means is "if e can evaluate to v, then [[ e ]] can evaluate a v' that is related to v." But that is not the same as saying that "e and [[ e ]] always get the same answers."

Details like that that make me wonder if there's any way to get the fine distinction that you want here without using the big clunky conjunctions...

(I tried a couple times just now to come up with a cleaner proposition but have not succeeded yet.)

Loren said...

It seems to me that what you really want is a universal, not an existential, quantification:

forall v. (e => v <=> (exists v'. v ~ v' and [[e]] => v'))

(Sorry if this appears twice—the original one didn't seem to ‘take’.)