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.)
Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.

Name

E-mail

Website

Comment