do i have to prove a deterministic lemma and a final lemma?

Stream: new members

[Huỳnh Trần Khanh]

the LoVe repository states that i should prove these two lemmas to make sure that my machine model is sane—why?

[Huỳnh Trần Khanh]

https://github.com/blanchette/logical_verification_2020/blob/master/lean/love08_operational_semantics_demo.lean#L475 https://github.com/blanchette/logical_verification_2020/blob/master/lean/love08_operational_semantics_demo.lean#L429

[Huỳnh Trần Khanh]

alright off for lunch! i'll read your responses later

[Mario Carneiro]

You don't have to prove a determinism lemma, but it is good to do so if your semantics is deterministic because it is easier to reason with a deterministic semantics

[Mario Carneiro]

you can conceptualize a deterministic state function as a sequence of steps in a line

[Mario Carneiro]

a nondeterministic state function has a tree of steps, so when you talk about eventually reaching some state you have to be careful about whether you mean that all paths through the tree end in a terminal state, or just one does, or for every node in the tree there exists a path to some terminal state

[Mario Carneiro]

the second theorem is often not true; a state which does not step but is also not a final state is called a stuck state and usually indicates some kind of error condition. The normal way this theorem is stated is that if some typing condition on the program holds, then the corresponding machine state is not stuck, and it is called the "progress lemma"