search

Deducteam / Dedukti-standard

This repository aims to provide documents which describe the Dedukti standard
0 stars 0 forks source link

Legacy terms #5

Open 01mf02 opened 2 years ago

01mf02 commented 2 years ago

The current standard draft gives a grammar for so-called "legacy terms" as follows:

t = "TYPE" | qid | t, t
  | "(", id, ":", t, ")", "=>", t
  | "(", id, ":", t, ")", "->", t
  | t, "->", t
  | "(", t, ")";

(See, by the way, how having even BNF as Markdown would make discussion easier? We could just copy-paste parts of the Dedukti standard here and have it syntax-highlighted in discussions. ^^)

Now these "legacy terms" are not what is described in syntax.bnf. In particular, the syntax for lambda-abstractions and dependent products diverges. However, my intuition thinks that "legacy" describes something that "is already there", in other words, the "state of the art". I therefore find the current wording a bit misleading.

Are the differences between the terms in syntax.bnf and the "legacy terms" described in the draft on purpose? If so, what is the reason for the differences?

01mf02 commented 2 years ago

A similar point could be made for rewrite rules: The draft currently states "Legacy Dedukti syntax" under that point, but the BNF allows something like [λ] a --> b, where the meaning of λ is unclear. Furthermore, this does not allow for [x: A] f x --> g x, because we cannot have typed variables à la x : A in the context.

francoisthire commented 2 years ago

I think the old syntax should be what is, the syntax of the dk tool suite which is the main tool using this syntax (sorry for Kontroli). AFAIK, the syntax of dk allows both [], [x], and [x:A] for rewrite rules contexts.

gabrielhdt commented 2 years ago

A similar point could be made for rewrite rules: The draft currently states "Legacy Dedukti syntax" under that point, but the BNF allows something like [λ] a --> b, where the meaning of λ is unclear. Furthermore, this does not allow for [x: A] f x --> g x, because we cannot have typed variables à la x : A in the context.

The lambda is the notation (given by the latex package) for the empty production.

01mf02 commented 2 years ago

I think the old syntax should be what is, the syntax of the dk tool suite which is the main tool using this syntax (sorry for Kontroli). AFAIK, the syntax of dk allows both [], [x], and [x:A] for rewrite rules contexts.

Do not worry about Kontroli, it accepts precisely what you described as rewrite rule contexts, namely [], [x], and [x:A]. :) And it also accepts the "old terms" of Dedukti (unlike in early 2020).

But you are only talking about what the old syntax should be. Should the new syntax diverge from this in your opinion?