Which description is correct?

[waddlaw]

Question: expression and predicate syntax.

Readme in liquidhaskell repo

expression

e := v                      -- variable
   | c                      -- constant
   | (e + e)                -- addition
   | (e - e)                -- subtraction
   | (c * e)                -- multiplication by constant
   | (v e1 e2 ... en)       -- uninterpreted function application
   | (if p then e else e)   -- if-then-else

predicate

p := (e r e)          -- binary relation
   | (v e1 e2 ... en) -- predicate (or alias) application
   | (p && p)         -- and
   | (p || p)         -- or
   | (p => p)         -- implies
   | (not p)          -- negation
   | true
   | false

But, this tutorial is below:

expression

    e := v                   -- variable
       | c                   -- constant
       | e + e               -- addition
       | e - e               -- subtraction
       | c * e               -- linear multiply
       | v e1 e2 ... en      -- uninterpreted function application

predicate

    p := true
       | false
       | e r e           -- atomic binary relation
       | v e1 e2 ... en  -- predicate application
       | p  && p         -- and
       | p  || p         -- or
       | p ==> p         -- implies
       | p <=> p         -- if and only if
       | not p           -- negation

Both of a bit different. Which is correct?

[ranjitjhala]

I think the only difference between the two is that the parentheses are explicit in the LH README? Normally, you shouldn't need the parentheses but if there is any ambiguity, use it to avoid confusion. e.g. with a && b || c I _think_ the precedences work the way you expect, i.e. && binds more tightly than || but I always write (a && b) || c just to be sure :)

…

On Tue, Oct 24, 2017 at 9:46 PM, Shinya Yamaguchi ***@***.***> wrote: Question: expression and predicate syntax. Readme in liquidhaskell repo <https://github.com/ucsd-progsys/liquidhaskell#formal-grammar-of-refinement-predicates> expression e := v -- variable | c -- constant | (e + e) -- addition | (e - e) -- subtraction | (c * e) -- multiplication by constant | (v e1 e2 ... en) -- uninterpreted function application | (if p then e else e) -- if-then-else predicate p := (e r e) -- binary relation | (v e1 e2 ... en) -- predicate (or alias) application | (p && p) -- and | (p || p) -- or | (p => p) -- implies | (not p) -- negation | true | false But, this tutorial is below: expression e := v -- variable | c -- constant | e + e -- addition | e - e -- subtraction | c * e -- linear multiply | v e1 e2 ... en -- uninterpreted function application predicate p := true | false | e r e -- atomic binary relation | v e1 e2 ... en -- predicate application | p && p -- and | p || p -- or | p ==> p -- implies | p <=> p -- if and only if | not p -- negation Both of a bit different. Which is correct? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#53>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOKtZreyyOZFTP4NBCK-dtseg0CmIks5svr0tgaJpZM4QFbkb> .

[waddlaw]

@ranjitjhala Thanks for your reply.

I think the only difference between the two
is that the parentheses are explicit in the
LH README?

Yes of course.
And more, I think that (if p then e else e) of expression is different from LH README.
Also ==>, p <=> p of predicate.

Thank you.

[waddlaw]

I think that is correct predicate syntax below:

p := (e r e)          -- binary relation
   | (v e1 e2 ... en) -- predicate (or alias) application
   | (p && p)         -- and
   | (p || p)         -- or
   | (p => p) | (p ==> p)         -- implies
   | (p <=> p)
   | (not p)          -- negation
   | true | True
   | false | False

To verified, I used liquid v0.8.0.5.
Let me clarify my understanding here.Is my understanding correct?

[ranjitjhala]

That is correct, thanks!

…

On Mon, Nov 6, 2017 at 12:36 AM, Shinya Yamaguchi ***@***.***> wrote: I think that is correct predicate syntax below: p := (e r e) -- binary relation | (v e1 e2 ... en) -- predicate (or alias) application | (p && p) -- and | (p || p) -- or | (p => p) | (p ==> p) -- implies | (p <=> p) | (not p) -- negation | true | True | false | False To verified, I used liquid v0.8.0.5. Let me clarify my understanding here.Is my understanding correct? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#53 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOP_JGvoGmcl67fKM03XHQmKt52-zks5szsT0gaJpZM4QFbkb> .

[waddlaw]

Can I update the document?
https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/02-logic.lhs#L106

[ranjitjhala]

Yes please, that would be most welcome! Thanks!

…

On Tue, Nov 7, 2017 at 6:06 AM, Shinya Yamaguchi ***@***.***> wrote: Can I update the document? https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/02- logic.lhs#L106 — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#53 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOE2SnhNFrJCGf0-vZZE2kCQsQT06ks5s0GPNgaJpZM4QFbkb> .

[waddlaw]

Merged. closing this issue.