No. To clarify, we’re not reducing any of the atomic operators of the language—e.g. we wouldn’t replace (0 == 0) ? 0 : 1 with 0. As written, that’s not a beta-reduction. If the ternary operator were defined as a function within the language itself, then we could beta-reduce it, but that wouldn’t give us “0”—it would give us some larger expression, containing “0 == 0“, “0”, and “1”.
Actually, thinking about it, here’s something which I think is equivalent to what I mean by “expand”, within the context of lambda calculus: beta-reduce, but never drop any parens. So e.g. 2 and (2) and ((2)) would not be equivalent. Whenever we beta-reduce, we put parens around any term which gets substituted in.
Intuitively, we’re talking about a notion of equivalence between programs which cares about how the computation is performed, not just the outputs.
No. To clarify, we’re not reducing any of the atomic operators of the language—e.g. we wouldn’t replace (0 == 0) ? 0 : 1 with 0. As written, that’s not a beta-reduction. If the ternary operator were defined as a function within the language itself, then we could beta-reduce it, but that wouldn’t give us “0”—it would give us some larger expression, containing “0 == 0“, “0”, and “1”.
Actually, thinking about it, here’s something which I think is equivalent to what I mean by “expand”, within the context of lambda calculus: beta-reduce, but never drop any parens. So e.g. 2 and (2) and ((2)) would not be equivalent. Whenever we beta-reduce, we put parens around any term which gets substituted in.
Intuitively, we’re talking about a notion of equivalence between programs which cares about how the computation is performed, not just the outputs.