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

[tlaplus] Beta Reduction

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 [1] is the closest mention of it that I see appearing in the tools.


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