[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
For the relationship to the OP, skip below the line. No need to read the whole
email.
> On May 19, 2021, at 9:52 PM, Jason Gross <jasongro...@gmail.com> wrote:
>
> I don't understand how this semantics works; it seems to me that it
> invalidates the normal reduction rules.
The ideas that Gabriel mentioned date back to Tim Griffin (POPL ’89) and Chet
Murthy (Cornell dissertation, ’90). They based their work on practical operators
with reduction rules that are a tad unusual if you’re stuck in “downwards is
the
way to go” mentality (thinkingCS trees here).
So here is an illustrative example [*]:
f (call/cc a) —> call/cc (\k.k (f (a (\x.k (f x))))
where f is a value (lambda), a arbitrary
The call/cc operator (and equivalent) exists in a bunch of programming
languages.
Spiritually, it originated with Scheme, thought Steele and Sussman introduced
`catch`
a variant of Reynolds `escape` operator (frim around the same time). The two
are
equivalent to `catch` and syntactic sugar for `call/cc`: escape k e == call/cc
(\k.e)
You can see that the type of call/cc is Peirce’s law.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - - - -
But let’s pop out a level to the original question. I’ll start with how Griffin
found
this idea. In ’88, I showed him `call/cc` and its type. He exclaimed:
“But that this can’t compute. It’s Perice’s law.”
Then I explained the reduction rules and, as a Constable student, he had the
predictable reaction. So he worked it all out and submitted to POPL and
the reaction of the French types-and-logic researchers was also predictable.
Fortunately, Murthy picked up and wrote a whole dissertation. [**]
I consider this little anecdote important. It tells us that we should NOT be
glued to the idea that what we know about the seemingly tight connection
between logic and computation is all there is too programming. Let people
explore programming "in the wild" and perhaps we will find a few more such
neat surprises and perhaps we will need to expand our understanding of logic.
— Matthias
;; - - -
[**] To their credit, they also worked out the relationship to the translations
Thomas sketched out in an upstream post. To find this literature, Tim Griffin
had to get to know the Rice football stadium.
[*] The reduction rules go back to my dissertation, though as usual, a month
after
turning it in, I found vastly simpler ones. Due to the printer-queue backlog at
TCS,
the simple ones were published 4 years later. See Felleisen and Hieb TCS 91 for
details.
— Yes, from then in, I presented only the “evaluation context semantics” or
“reduction
semantics”or “small step semantics” (not my name) because it was easier to
understand
and use for the typical POPL attendee.
