8
votes
Accepted
Do we care about confluence because of unique normal forms?
I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for ...
- 5,038
5
votes
Moggi's computational metalanguage
It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For ...
- 27.5k
4
votes
For what languages is there already a theory of observational equivalence?
A compositional denotational semantics $[\![ {-} ]\!]$ of a programming language (a domain-theoretic or game-theoretic one, for instance) is adequate if semantically equal terms imply that they are ...
- 27.5k
3
votes
Accepted
What is contextual equivalence ignoring non-termination called?
(This is an extended comment).
I may be misreading your definitions, but it seems to me that the relation you introduce, let us call it $\simeq$, is not an equivalence relation because it is not ...
- 5,038
3
votes
Why structural rules define the "smallest relation" satisfying the rules?
"Smallest relation with property $\mathscr{P}$" just means "subset of every relation with property $\mathscr{P}$" - thinking of a relation as a set of ordered pairs. Basically, we ...
- 505
2
votes
Accepted
Moggi's computational metalanguage
I still don't quite understand what having a value means, but just considering the question of "can we give up the eta rule for monads", the answer is yes, this is an entirely reasonable thing to ...
- 32.1k
2
votes
For what languages is there already a theory of observational equivalence?
The domain and model theories of PTSes hasn't been explored all that much I'm afraid. One detailed source is Thomas Streicher's PhD work: Semantics of Type Theory. He gives category theoretic ...
- 13.5k
Only top scored, non community-wiki answers of a minimum length are eligible