On Mon, Oct 21, 2019 at 12:37 PM Brian Nguyen <[email protected]> wrote:
> As far as I can tell, the Metamath language has been restricted more and > more over time: first "mandatory spaces between tokens", then in 2006 > (according to the book) "math symbols and statement labels share > namespace", and then "variable types are global" (a restriction I've never > seen in any other computer language). Even C#, which disallows variable > shadowing, doesn't have this. > This is a rather bizarre comparison. Have you seen the spec of C#? I haven't, but I'm pretty sure it doesn't fit on 2 pages. > I believe that although the first restriction simplified the language > greatly (by not special casing certain characters and tokens), the later > restrictions complicate both the machine side (verifier development) and > the human side (inputting axioms and theorems) of Metamath. > > - Without the namespace restriction I could manage statements and math > symbols with two list variables. With the restriction I must either check > that the two namespaces do not intersect or use one list for both and > annotating whether an identifier refers to a symbol or a proposition. It is > supposedly added to make writing certain parsers easier, but in my opinion > some other parsers are more complicated. > > Or you store them in separate lists and call it a day. You have the *option* to store them in the same list but you don't have to. > > - The "variable types are global" restriction is outright silly. The > purpose of variable scoping is to declare that variables with the same name > in different scopes are different variables. This also requires verifiers > keep track of local variable scope and global variable types *at the > same time*. Isn't it stupid? This also wreaks havoc with included > files, which may declare common variable names with unrelated types, a > problem exacerbated by the lack of a real module/namespace system. > > It makes variable tracking easy: You just ignore scopes entirely, and allow redefinition of variables. Actually, I would prefer that we go all the way and just make variables completely top level and global. There is no loss of expressivity, and local variables in Metamath are clunky at best. (Why do you have to name the variable hypotheses?) I think that to have proper handling of local variables in metamath would require a new language <https://github.com/digama0/mm0>. The restriction was only added as a way to acknowledge existing practice. set.mm and all the other major mm databases have had almost entirely only global variables for years, with exceptions only for things like introducing a variable before the typecode is properly defined. > > - The implicit disjoint variable restriction is even worse. The > Metamath program developed by Norman Megill in C clearly has the ability to > determine which variables are dummy. Also, "implicit" distinct variables > don't even exist because they don't matter to users of the theorem (after > all, you can reprove the theorem under a different name without the > redundant disjoint restrictions with a short proof referencing the original > theorem). > > This is a deliberate aesthetic choice on Norm's part. It is being more explicit about what you mean. > Even if we assume that these restrictions make writing tools simple, the > simplest solution is no code, no computer, no automation at all and letting > people write and verify proofs in the informal style, which defeats the > entire point of Metamath. > This is a straw man. Metamath is entirely the opposite of this: it is an *extremely explicit* style of writing proofs that is optimized for easy verification. > Also repeatedly making backwards incompatible changes to a program for no > good reason and without a conversion/migration tool is poor practice. We > will never know how many private databases were, are and will be broken by > the introduction of the restrictions. > We'll never know (or care) unless they tell us. As far as I can tell this has broken no one's code. Anyway, I was trying to axiomatize the not-free predicate as follows: If a > variable x does not occur in an expression S then x is not free in S. If S > is a quantifier expression (of the form forall x: P, exists x: P, et > cetera) then x, being quantified over is not free. If S1, S2 are arbitrary > sequences of symbols, neither contains x, S is an expression in which x is > not free and the sequence S1 S S2 is an expression then x is not free in S1 > S S2. > I see. To make this work you would need to define a type of "arbitrary sequences of symbols" and use that type for S1 and S2. I recommend against it, because the syntax ambiguity will bite you later. You can do it using well formed expressions if you have axioms for each syntax constructor; that's what I did in my message. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs40Z45_Wm%2B6PP36uDBwRuzNszoPVtWgbO6a%2B8ozE8Jhg%40mail.gmail.com.
