« 2+2=4
Towards Proof-Irrelevant Equality »

Minutes

Meeting:

  • Thorsten should type:
    1. darcs get http://sneezy.cs.nott.ac.uk/darcs/term
    2. cd term
    3. chmod +x Setup.hs
    4. ./Setup.hs configure --prefix=$HOME
    5. ./Setup.hs build
    6. ./Setup.hs install --user
    7. (and providing $HOME/bin is in your path:) epigram
  • The next job in term is to build equality in these steps:
    1. Propositional equality
      $\Rule{\va\hab\vA\quad\vb\hab\vB}{\va=\vb\hab\Type}\;\;\Axiom{\DC{refl}\hab\va=\va}$
      coersions between equal types (and the proof that these are coherant)
      $\AR{\Rule{\va\hab\vA\quad\vq\hab\vA=\vB}{\va\ [\vq\rangle\hab\vB}\smallskip\\ \Rule{\va\hab\vA\quad\vq\hab\vA=\vB}{\va\ [\![\vq\rangle\hab\va\ [\vq\rangle=\va}}$
      and the structural rule for application
      $\Rule{\vp\hab\vf=\vg\quad\vq\hab\vs=\vt}{\vp\,^=\vq\hab(\vf\ \vs)=(\vg\ \vt)}$
    2. Proof-irrelevance for equality, to do this right we need to decide equality during evaluation (if we do not have a proof of an equation but it’s homogeneous, then we win anyway). The upshot is Equality.lhs and eval from Term.lhs need to be in the same file.
    3. Observational equavalence, at some point (sooner rather than later) we’ll include the structural rule for $\lambda$:
      $\Rule{\AR{\VV{t_0}\hab\forall\VV{x_0}\hab\VV{S_0}\Rightarrow\VV{T_0}\\ \VV{t_1}\hab\forall\VV{x_1}\hab\VV{S_1}\Rightarrow\VV{T_1}\\ \vS\hab\VV{S_0}=\VV{S_1}\\ \left(\Rule{\VV{x_0}\hab\VV{S_0}\quad\VV{x_1}\hab\VV{S_1}\quad\vx\hab\VV{x_0}=\VV{x_1}} {\VV{t\;x_0\;x_1\;x}\hab\VV{t_0\ x_0}=\VV{t_1\ x_1}}\right)}}{\lambda^=\vS\ \vt\hab(\lambda\VV{x_0}\hab\VV{S_0}\Rightarrow\VV{t_0\;x_0})=(\lambda\VV{x_1}\hab\VV{S_1}\Rightarrow\VV{t_1\;x_1})}$
      Thorsten pointed out that is rule can be derived from substution of equals for equals plus the more primitive:
      $\Rule{\VV{t_0},\VV{t_1}\hab\forall\VV{x}\hab\VV{S}\Rightarrow\VV{T}\quad\vf\hab\forall\vx\hab\vS\Rightarrow\VV{t_0\;x_0}=\VV{t_0\;x_0}}{\lambda^=\vf\hab(\lambda\VV{x}\hab\VV{S}\Rightarrow\VV{t_0\;x})=(\lambda\VV{x}\hab\VV{S}\Rightarrow\VV{t_1\;x})}$
      Having this gives OTT a simpler core, but Conor prefers the first version because it is easier to program with.

This entry was posted on Tuesday, January 17th, 2006 at 11:34 am and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

Leave a Reply