Beta Reduction
27 views
Skip to first unread message
Willy Schultz
Nov 16, 2021, 12:07:19 AM11/16/21
to tlaplus
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
Op(e1,...,en)
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 [1] is the closest mention of it that I see appearing in the tools.
Will
Reply all
Reply to author
Forward
0 new messages