[tlaplus] Beta Reduction

[Willy Schultz <will62794@xxxxxxxxx>]

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

[1] https://github.com/tlaplus/tlaplus/blob/d977051118f63b9c97d7d4c4d6af27183971ada3/tlatools/org.lamport.tlatools/src/tla2sany/semantic/LevelNode.java

-- 
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.