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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Mon, 1 Jul 2019 06:32:28 -0400*References*: <ded66eba-ffa2-4ba0-9146-06d1e4f00210@googlegroups.com> <4a27f599-5671-4db2-b9b6-b831b90d5340@googlegroups.com>

Thank you for the clarification.

Paul

On Monday, July 1, 2019, Leslie Lamport <tlaplus.ll@xxxxxxxxx> wrote:

-- On Monday, July 1, 2019, Leslie Lamport <tlaplus.ll@xxxxxxxxx> wrote:

--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 writingn == 15because 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 declarationor 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 ofits declaration. This assumes thatRECURSIVE 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 allowrecursive operator definitions.This demonstrates the difficulty of making correct statements in aninformal language like English. Thank you for pointing it out.Leslie

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/jXBjiUjfXqY/ .unsubscribe

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com .

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 .

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/CAHeFUE9JV3ihvXr1SFACroUupFar_02AfKGWwtj3q_3hdaHqHw%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

**References**:**[tlaplus] Which symbols need to be defined? (new to TLA+)***From:*Saswata Paul

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

- Prev by Date:
**[tlaplus] Some edges are missing** - Next by Date:
**Re: [tlaplus] Some edges are missing** - Previous by thread:
**[tlaplus] Re: Which symbols need to be defined? (new to TLA+)** - Next by thread:
**[tlaplus] Some edges are missing** - Index(es):