Can you express evaluation order using big-step semantics? For example, in a simple language consisting of only if t then t else t and true and false, we can decide to only step a if then else to one of its branches if its branches are already values.Can big-step semantics express the same thing?
Can big-step semantics express evaluation order?
programming languages;type theory
No, you cannot express evaluation order using big-step semantics.Borrowing from Benjamin Pierce: big-step semantics is a multi-step evaluation relation that directly formulates the notion of this term evaluates to that final value. So it cannot impose the kind of evaluation order you describe.Also keep in mind what the horizontal bar represents. Again borrowing from Pierce: If we have established the statements in the premise(s) listed above the line, then we may derive the conclusion below the line. It would not make sense to impose an ordering on the premises to draw the conclusion.