[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Here is a proof that values don't step:
https://urldefense.com/v3/__https://pastebin.com/raw/V9Kg0cY4__;!!IBzWLUs!DI_iHIlT1E8rdhB4G9G-Wm5cLeF8loOevBXfeUhqHo4zaA1zOdGzKrCuHt_3u2trbh_ZLMAUCho$
The relevant parts are:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
@Jules: I think you're right and I was wrong. There's no need to
define the eval ctxt typing *intensionally*, as I have been doing. I
might as well define it *extensionally* (which is more my style
anyway, but somehow
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> I managed to carry out a proof along the lines described by Derek and Jules,
> but it used more ink (and more think!) than my original proof using a
> congruence rule for each constructor. In this, as in much else, I
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I had previously only addressed the first part of this only to Philip
Wadler, so I reproduce it here:
Compcert uses evaluation contexts:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Philip,
Here's a hacky (but simple!) way that works on my end, try defining _[_]
like this
```
_[_]′ : Frame → Term → Term × Term
(□· M) [ L ]′ = L , M
(·□ V _) [ M ]′ = V , M
_[_] : Frame → Term → Term
F [ T ]
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, Phil.
Yes, there is a way to make the single congruence rule work. See for
example the way I set things up in my Semantics course notes (see
Section 1.2):
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Most mechanised formulations of reduction systems, such as those found in
Software Foundations or in Programming Language Foundations in Agda, use
one congruence rule for each evaluation context:
ξ-·₁ : ∀ {L L′ M}
