[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Which symbols need to be defined? (new to TLA+)



Dear Mr. Sawasta Paul,

You have made a remarkably astute observation.  In retrospect, I'm
astonished that no one has noticed this before.  The rule that a
symbol can be used only after it is declared or defined makes no
sense, since it makes it impossible to declare or define any symbol.
For example, that rule forbids writing

  n == 15

because n isn't defined until after that statement, so it would not be
allowed to appear in that statement.  One might attempt to correct the
rule to say that a symbol may appear only in or after its declaration
or definition.  However, that would forbid this _expression_

   {n+1 : n \in Nat}

(which equals the set of positive integers) because "n+1" comes before
"n \in Nat", which locally declares n.

The precise statement of the rule is that a symbol that is not a built-in
TLA+ symbol can appear only in its declaration or within the scope of
its declaration.  This assumes that

   RECURSIVE F(_)

is considered to be the declaration of F, and any rule about not defining
a symbol that's already declared must be appropriately weakened to allow
recursive operator definitions.

This demonstrates the difficulty of making correct statements in an
informal language like English.  Thank you for pointing it out.

Leslie

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4a27f599-5671-4db2-b9b6-b831b90d5340%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.