Hello Neil,
I had liked your logic examples concerning decidability of propositions,
stability and the Peirce law as a nice addendum to the logic section of
Conor's and Peter Hancock's lecture notes, which are really worth a read
as they take the epigram systems Mise en Scène approach to program
development further than ever.
But concerning your definition of addition...
* Am 14.12.06 schrieb neil:
------------------------------------------------------------------------------
[If we have:]
------------------------------------------------------------------------------
( n : N !
data (-------! where (----------! ; !------------!
! N : * ) ! zero : N ) ! succ n : N )
------------------------------------------------------------------------------
[we can happily define:]
------------------------------------------------------------------------------
( p, q : N !
! !
! ( x, y : N ! !
! !-----------! !
! ! C x y : * ) !
! !
! d : C zero zero !
! !
! ( n : N ; u : C zero n ! !
! !-------------------------! !
! ! e n u : C zero (succ n) ) !
! !
! ( m : N ; v : C m zero ! ( r, s : N ; w : C r s ! !
! !-------------------------! ; !-------------------------------! !
! ! f m v : C (succ m) zero ) ! g r s w : C (succ r) (succ s) ) !
let !------------------------------------------------------------------!
! dblnatrec p q C d e f g : C p q )
dblnatrec p q C d e f g <= rec p
{ dblnatrec p q C d e f g <= case p
{ dblnatrec zero q C d e f g <= rec q
{ dblnatrec zero q C d e f g <= case q
{ dblnatrec zero zero C d e f g => d
dblnatrec zero (succ q) C d e f g
=> e q (dblnatrec zero q C d e f g)
}
}
dblnatrec (succ p) q C d e f g <= rec q
{ dblnatrec (succ p) q C d e f g <= case q
{ dblnatrec (succ p) zero C d e f g
=> f p (dblnatrec p zero C d e f g)
dblnatrec (succ p) (succ q) C d e f g
=> g p q (dblnatrec p q C d e f g)
}
}
}
}
------------------------------------------------------------------------------
[We can now define addition using dblnatrec to do the refinement for us:]
------------------------------------------------------------------------------
( a, b : N !
let !-------------!
! add a b : N )
add a b <= dblnatrec a b
{ add zero zero => zero
add zero (succ n) => succ n
add (succ m) zero => succ m
add (succ r) (succ s) => succ (succ (add r s))
}
------------------------------------------------------------------------------
[Not the first definition of addition you thought of, and there is !
!certainly some redundancy in there but... !
! !
!So, let's do some exercises. Fire up epigram, load the definitions so!
!far and define: ]
------------------------------------------------------------------------------
( A : * ; a, b : A !
data !-------------------! where (---------------!
! Eq A a b : * ) ! eq : Eq A a a )
------------------------------------------------------------------------------
[and this handy lemma:]
------------------------------------------------------------------------------
( p : Eq N n m !
let !-----------------------------------!
! eqsucc p : Eq N (succ n) (succ m) )
eqsucc p <= case p
{ eqsucc eq => eq
}
------------------------------------------------------------------------------
[and the definition of addition that you probably did first think of:]
------------------------------------------------------------------------------
( n, m : N !
let !--------------!
! plus n m : N )
plus n m <= rec n
{ plus n m <= case n
{ plus zero m => m
plus (succ n) m => succ (plus n m)
}
}
------------------------------------------------------------------------------
[Now, try to elaborate:]
------------------------------------------------------------------------------
( n, m : N !
let !------------------------------------------!
! plussym n m : Eq N (plus n m) (plus m n) )
plussym n m []
------------------------------------------------------------------------------
[using rec and case on n and m to refine the problem.!
! !
!Now see what happens when you elaborate: ]
------------------------------------------------------------------------------
( n, m : N !
let !---------------------------------------!
! addsym n m : Eq N (add n m) (add m n) )
addsym n m []
------------------------------------------------------------------------------
[using dblnatrec n m to refine the problem. !
! !
!OK, so that was a bit of a cheat, since we did not solve the same!
!problem. !
! !
!Now elaborate: ]
------------------------------------------------------------------------------
[ ( n, m : N !!
!let !------------------------------------------!!
! ! plussym n m : Eq N (plus n m) (plus m n) )!
! !
! plussym n m [] ]
------------------------------------------------------------------------------
[using dblnatrec n m to refine the problem. You get exactly the same!
!sub-problems as when refining using rec and case, but you get them !
!more easily. !
! !
!You can also elaborate: ]
------------------------------------------------------------------------------
( n, m : N !
let !-------------------------------------------!
! addisplus n m : Eq N (add n m) (plus n m) )
addisplus n m []
------------------------------------------------------------------------------
[(Proving the transitivity of equality helps here, of course.) !
! !
!There is lots more fun to be had here, and is clearly a lot more to!
!explore on how to use epigram to define induction schemas to make !
!programming easier. This is one of the features of epigram which I !
!think is really attractive. ]
------------------------------------------------------------------------------
... I'd like to note that you've lost definitional left-absorption this
way:
------------------------------------------------------------------------------
inspect (lam n : N => add zero n) => (lam n => add zero n) : all n : N => N
------------------------------------------------------------------------------
inspect (lam n : N => plus zero n) => (lam n => n) : all n : N => N
------------------------------------------------------------------------------
Moreover, you can define addition which easily commutes directly via
case analysis without giving up left-absorption.
------------------------------------------------------------------------------
( a, b : N !
let !-------------!
! add a b : N )
add a b <= rec a
{ add a b <= case a
{ add zero b => b
add (succ a) b <= case b
{ add (succ a) zero => succ a
add (succ a) (succ b) => succ (succ (add a b))
}
}
}
------------------------------------------------------------------------------
inspect (lam n : N => add zero n) => (lam n => n) : all n : N => N
------------------------------------------------------------------------------
( a, b : N !
let !--------------------------------!
! addsym a b : add a b = add b a )
addsym a b <= rec a
{ addsym a b <= case a
{ addsym zero b <= case b
{ addsym zero zero => refl
addsym zero (succ b) => refl
}
addsym (succ a) b <= case b
{ addsym (succ a) zero => refl
addsym (succ a) (succ b) => eqsucc (eqsucc (addsym a b))
}
}
}
------------------------------------------------------------------------------
This only reassures me why I prefer case analysis over giving a matrix
of constructors in one go.
But it could be worse. With your definition the behaviour is at least
directly readable from the program, which it would not if it had been
mine compiled away from a definition given by pattern matching (with a
take-the-first-match semantics).
Cheers,
Sebastian
