[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Beta Reduction
- From: Willy Schultz <will62794@xxxxxxxxx>
- Date: Mon, 15 Nov 2021 21:07:19 -0800 (PST)
- Ironport-hdrordr: A9a23:+HVN7ag0FiHtAqVBvEJkTvT8kXBQXtIji2hC6mlwRA09TyX4rbHMoB1/73TJYVkqNU3I9ertBED4ewK4yXcX2+ks1NWZMjUO0VHAROtfBODZogEIdReQysdtkZ1KXINaYeeAb2RHsQ==
From Specifying Systems Chapter 17.1.2, my understanding is that beta-reduction refers to the procedure of replacing the identifiers of a lambda _expression_ with appropriate, corresponding expressions e.g. for a lambda _expression_
LAMBDA p1,...,pn : exp
that represents the operator Op, we have that
equals the result of replacing pi in exp with ei for all 1...n.
My question is whether this beta-reduction procedure is implemented directly in TLC or SANY. I am wondering if it is possible with any of the current tools to take a spec and reduce it to a form such that all defined operators are substituted with their full definitions. This  is the closest mention of it that I see appearing in the tools.
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b93c7aae-1d72-478a-a9a6-32b6debb0d90n%40googlegroups.com.