2
$\begingroup$

I'm reading "Program=Proof" by Samuel Mimram, and they use a notation for defining a formal language that I'm not familiar with.

Here is how "Program=Proof" defines a formal language of Propositional Logic:

Here is how "Program=Proof" defines a formal language of λ-calculus:

On the other hand, I'm more used to formal languages defined in the following way (this example is from Wikipedia):

Do I understand it right that this rule:

A, B ::= X | A ⇒ B | A ∧ B | ⊤ | A ∨ B | ⊥ | ¬A

can be rewritten to a more traditional:

S → X | S ⇒ S | S ∧ S | ⊤ | S ∨ S | ⊥ | ¬S

And this rule:

t, u ::= x | t u | λx.t

can be rewritten to a more traditional:

S → x | S S | λx.S

without any loss of information?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

Yes, I think that's basically the intent. I guess the book is trying to write grammars without grammatical symbols. For me, it's abuse of notation, but that's pretty common.

Because there is no formal notation for grammatical symbols, the grammar doesn't really express the fact that $A$ and $B$ are formulas, $X$ is a propositional variable, and $\{⇒, ∧, ⊤, ∨, ⊥, ¬\}$ are syntactic tokens. That needs to be expressed in the narrative (or left to the readers' intuitions), but that's probably a quibble since the meaning is more or less evident.

A similar quibble could be raised about the author's handling of operator associativity. But I don't think that this is a text about parsing theory; it's more about programs as formal semantic structures. It's equally possible to read the "grammars" as type declarations for expression components, also a reading which requires a certain generosity but nonetheless offers some insights.

Improve this answer
$\endgroup$
6
  • 3
    $\begingroup$ It's not "abuse of notation", just notation that you're not familiar with. $\endgroup$
    – Yuval Filmus
    Jun 25 at 19:27
  • 2
    $\begingroup$ @YuvalFilmus: Can you make it precise? As notation, I mean. What it expresses is precise, but mechanically translating that notation to the underlying meaning requires you to fill in a bunch of lacuna which are left to a non-formal narrative explanation. A precise version would have parentheses or use prefix notation. That's not a criticism; this is not about formal language theory. If it conveys the ideas, fine. But at some level I react to calling this a grammar the same way I react when I see $f(x) = O(g(x))$; it's customary; it's understood; and yet as notation, it's unsatisfying. $\endgroup$
    – rici
    Jun 25 at 19:58
  • 1
    $\begingroup$ If you have objects $A$ and $B$, then you can create from them other objects: $X$, $A \Rightarrow B$, and so on. Think type theory or logic. $\endgroup$
    – Yuval Filmus
    Jun 25 at 20:33
  • 1
    $\begingroup$ @Yuval: Yes, that's why I said «It's equally possible to read the "grammars" as type declarations». I do get what it means, but it seems to me that it skates over the distinction between formulas in PL and the metalanguage used to describe formulas. $A$ and $B$ are not symbols in PL, and neither is $X$. So what is $A\implies B$? And what does the symbol $::=$ mean in $A, B ::= A\implies B$? (which I think should really be $A, B ::= (A \implies B)$ All this is probably pedantry, like insisting that a function can not be equal to a set of functions. But this Q shows that confusion is possible. $\endgroup$
    – rici
    Jun 25 at 23:02
  • 1
    $\begingroup$ The first time I saw this I was confused too, but it seems just another "dialect". A colleague of me teaches introductory formal logic and he specifies syntax of propositional logic in a similar way: $\varphi ::= p \mid \bot \mid \varphi \land\varphi \mid \varphi\lor\varphi \mid \varphi\to\varphi \mid (\varphi) $. Probably from type theory or formal semantics, I do not know. $\endgroup$
    – Hendrik Jan
    Jun 26 at 16:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.