search

salmans / Razor

5 stars 0 forks source link

Augmentation Syntatic Sugar #73

Open salmans opened 9 years ago

salmans commented 9 years ago

In the key/card example, I am trying to augment the first model of the first query with the following fact: cardOf(e^3) = e^100 but Razor says that the input formula for augmentation is invalid. Is it an issue with the parser?

thedotmatrix commented 9 years ago

cardOf(e^3) is e^4 in that case I believe. e^4 = e^100 should work as a valid augmentation.

again, the repl currently disallows augmentations in the form f(e1) = e2... as f is a partial function and f(e1) may not exist yet, putting it in the "adding existential quantifier support for augmentation" issue

salmans commented 9 years ago

I remember we talked about this case but I thought that was an issue when we set the value of a function applied to an existing element (which already doesn't have any value in the function) to another existing element. For instance cardOf(e^6) = e^4. But anyway, here is what I think:

  1. In the first model, the user doesn't see anything about the cardOf(e^4). That's why we can't expect the user to use e^4 as the handle to cardOf(e^6).
  2. We currently do support existential quantifiers (of course in a weird way where the user mentions a new element in the augmentation. I don't see any reason for the same approach not working to augment functional values. For instance here, we just should treat the function as if the user is augmenting the model with a (relationalized) fact cardOf(e^3, e^100).

I am not suggesting that we should fix these bug right now. Having said that, it is nice to fix it if it doesn't take too much time.

thedotmatrix commented 9 years ago

My apologies for not responding sooner; I got a delayed with some personal things. Took a look now... reusing your relationalizeX functions isn't as clear cut as I expected, mostly due to the counter monad being used.

I'd rather not make a more drastic change that we haven't discussed before tomorrow with this much time left. (I'm going to keep this sentiment for the other two issues as well). Sorry for any slight awkwardness that may come up in this situation, but I think that's better than me possibly breaking other more crucial functionality.

salmans commented 9 years ago

No problem! I completely agree with you. I have already finalized the version of Razor that I am using tomorrow; Razor is pretty stable and ready to go!

thedotmatrix commented 9 years ago

This comes down to a couple of mostly syntactic enhancements.

  1. exists x. P(x) := P()
  2. P(f(e^1)) := P(e^2), where f(e^1) = e^2; e^1 is in the domain of the partial function f
  3. P(f(e^1)) := exists x. P(x) & f(e^1)=x, e^1 is not in the domain of the partial function f