Mathematics and Computation

A blog about mathematics for computers

The troublesome reflection rule (TYPES 2015 slides)

Here are the slides of my TYPES 2015 talk “The troublesome reflection rule” with fairly detailed presenter notes. The meeting is  taking place in Tallinn, Estonia – a very cool country in many senses (it's not quite spring yet even though we're in the second half of May, and it's the country that gave us Skype).

Download slides: The troublesome reflection rule (TYPES 2015) [PDF].

Comments

Mike Shulman

Nice! A few comments/questions:

  1. Some of the notes on the RHS of the slides are cut off at the end.
  2. Doesn't the eta-rule together with the reflection rule give you function extensionality?
  3. Are you saying that the reflection rule is never applied (and, thus, an Eq-term in the context is never used) unless a hint explicitly instructs us to?
Andrej Bauer
  1. Fixed.
  2. Yes, see examples/funext.m31
  3. Yes, you get to choose which set of computation rules to use in each situation. (Of course, we plan to add flexible ways for manipulation of these.)
How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.