New answers tagged

2

The book that defines TLA+ is "Specifying systems" by Leslie Lamport. TLA+ is a language for writing mathematics (TLA+ is based on Zermelo-Fraenkel set theory). TLA+ includes temporal formulas, which can describe hardware and software systems. PlusCal is an algorithm language (user manual) that is translated to TLA+. So systems can be described ...


1

This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops. Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda calculus (with or without types: types don't affect evaluation), you want a quantity (a positive integer) that decreases at each reduction step. Such a quantity ...


Top 50 recent answers are included