HI,
On 13/12/2006, at 10:02 PM, Thorsten Altenkirch wrote:
Hi Neil,
sorry that as far as I can see nobody has yet replied to your
email. I certainly have been very busy recently.
Sounds you have run a very interesting course. Can you give some
more details on your symmetric definition of addition?
James and I had a short discussion on this so maybe it is also of
interest to other people, although I'm perhaps preaching to the
converted here.
One of the things which I wanted to show students was how you can
define your own induction schema and hence refinement operators in
epigram, and how doing this can really make solving problems a lot
simpler. The nicest example I could come up with was proving the
symmetry of addition.
Suppose n, m are Nats and you want to prove P(n, m). Well you expect
to do one induction on n, and give yourself the sub-problems of
proving P(0, m) and of proving P((s n), m) given P(n, m). In each of
these you do an induction on m to give yourself (eventually) the
tasks of proving P(0, 0); P(0, (s m)) given P(0, m); P((s n), 0)
given P(n, 0); P((s n), (s m)) given P(n, m). Perhaps you might have
chosen to do the induction on m first, and then the inductions on n.
It really doesn't matter which order you do them in as you get the
same sub-goals. But here is the neat thing which epigram lets us do:
we can define and use our own induction schema to capture this pattern.
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 []
! plussym n m : Eq N (plus n m) (plus m n) )
------------------------------------------------------------------------
----------------------------------
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 []
! addsym n m : Eq N (add n m) (add m n) )
------------------------------------------------------------------------
----------------------------------
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 []
! plussym n m : Eq N (plus n m) (plus m n) )
------------------------------------------------------------------------
----------------------------------
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 []
! addisplus n m : Eq N (add n m) (plus 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.
Btw, are you going to attend CATS in January?
Unfortunately not.
Cheers,
Thorsten
Best,
Neil
On 28 Nov 2006, at 23:33, neil wrote:
Hi Everyone,
More noise for this list!
I used Epigram in teaching this year, and, since summer is nearly
here I thought I'd give some feedback on my experiences. All of
this is very unscientific and subjective, so take with a pinch of
salt.
The class was a final year BSc Hons class (Snr Hons in Scottish
terms) in functional programming. Most NZ students leave at the
end of 3rd year, and usually only strong students stay on for 4th
year. The class also had some students who were taking taught
Master's degrees. These students have a wider range of abilities.
Before we started on Epigram we covered (relatively) practical
Haskell programming, and some lambda calculus. Some of the
students had taken a paper on computational logic, which focusses
on theorem proving and logic programming, but also covers Gentzen
systems.
With epigram I was aiming for several related goals:
1) introduce the Curry-Howard/Propositions as types/proofs as
programs idea, and give the flavour of programming in constructive
logic
2) let students experience epigram's interactive programming
environment
3) let students see dependent types doing something useful (or at
least something neat)
We did various things:
a) We gave the usual logical types, and Nats, lists, equality...
b) to get a flavour of the extra power of the type system we
started with lists and append in Haskell, and moved to defining
lists and append in type theory. Then we moved on to defining
vectors and exploring how we could use the type to express a full
specification for append.
c) to get a bit more of the flavour of programming constructively
we proved that very Nat is either even or odd. This is similar to,
and much simpler than, "either this string parses or it doesn't".
I gave the students an assignment which involved proving some
`logical' stuff and defining and proving that addition is
commutative.
The logic went from showing |- A & B -> B & A, up to showing that
A v -A |- --A -> A, and showing --A -> A |- A v -A does not hold,
and showing A v -A |- ((A -> B) -> A) -> A.
I gave them two definition for addition:
plus 0 m = m
plus n' m = (plus n m)'
and
add 0 0 = 0
add 0 n' = n'
add n' 0 = n'
add n' m' = (add n m)''
To permit the latter definition I gave them an elimination rule
(and consequently a new refinement operator). Proving that add is
commutative is a lot easier than proving that plus is.
The reaction of the students to epigram was, predictably, mixed. I
had feared that they would complain about the UI (none were very
experienced emacs users, for example) but none of them raised this
as an issue. Curiously, one of them expressed a dislike for the
style of incremental program development with rapid feedback! The
very best students got a lot out of working with epigram. Some of
the middle students found the harder assignment questions beyond
them, but some of the middle students really got the idea of
proofs as programs. At least one of the weaker students just
didn't understand what was going on.
I intend to use epigram again next year. Two obvious things which
I could improve are:
i) fewer logical examples, and more programming examples;
ii) more motivating examples of quite basic uses for dependent types;
Anyhow, I hope that this is useful to someone, and I'm happy to
discuss further with anyone interested. I guess that eventually
there is a paper on teaching programming in constructive type
theory constructively in this somewhere.
Cheers,
Neil
School of Mathematics, Statistics and Computer Science &
Centre for Logic, Language and Computation
Victoria University
P. O. Box 600
Wellington Tel +64 4 463 6732
New Zealand mailto:[EMAIL PROTECTED]
The information in this e-mail message is confidential and may
also be privileged. If you are not the intended recipient, please
notify the sender immediately and destroy any copies of this e-mail.
This message has been checked for viruses but the contents of an
attachment
may still contain software viruses, which could damage your
computer system:
you are advised to perform your own checks. Email communications
with the
University of Nottingham may be monitored as permitted by UK
legislation.
School of Mathematics, Statistics and Computer Science &
Centre for Logic, Language and Computation
Victoria University
P. O. Box 600
Wellington Tel +64 4 463 6732
New Zealand mailto:[EMAIL PROTECTED]
The information in this e-mail message is confidential and may also
be privileged. If you are not the intended recipient, please notify
the sender immediately and destroy any copies of this e-mail.
