Hi Yong
Yong Luo wrote:
Hi, Conor,
Since you use elimination rule on both arguments, I was expecting four cases
like Thorsten did in the previous email. Can we define the Ackermann
function like the following form?
ack x y = Elim_Nat ......
For example, plus can be defined as:
plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
That's exactly what's going on behind the scenes. Tell you what...
...the attached file now contains three definitions of the same
function. The first is as before. The second, ackFun, is the term you
asked for: we only get three cases, because the second elim only happens
in the suc case of the first. I've checked that all the laws hold
computationally by proving them with refl. The third version, acktual,
shows how Epigram actually does it: the type family ACK x y represents
computations of Ackermann's function, and its constructor, ret, just
packs up a pair of arguments and the corresponding answer; the function
call x y (ret x y n) => n
just unpacks the number. The idea is that you can read (call x y blah)
as a call to (acktual x y), provided you can find some blah which shows
that the computation is possible. Of course, we implement acktual by
showing that the computation is always possible. The definition is just
like ackFun, but you can see your pattern matching program in there:
each ret is a line of the program; each call is a recursive call,
explained by appeal to an inductive hypothesis whose type says which ACK
computations it's willing to perform. Moreover, when you run acktual on
open terms, you can read off the result of the pattern matching program,
just by translating (call x y blah) as (acktual x y): as you can see,
the blah is often large and boring.
The moral of the story is this: if you know how to do induction, you get
a programming language for free!
Meanwhile, as far as the majority function is concerned...
[For the uninitiated, this is G\'erard Berry's notorious counterexample
to the correspondence between pattern matching and case expressions when
operating over open terms, it goes like this
maj :: Bool -> Bool -> Bool -> Bool
maj True True True = True
maj True False b = b
maj False b True = b
maj b True False = b
maj False False False = False
Its patterns are clearly exhaustive and disjoint, but there is no tree
of case splittings which delivers those five cases, hence no Epigram
program maj which satisfies all five of those laws computationally.]
Exercise: find an Epigram definition of majority, extensionally equal to
maj) with fewer cases. You'll discover that some of the computation laws
for your solution only hold propositionally for Berry's definition.
When you compute with values, maj is (deliberately on Berry's part) a
very silly way to compute the result: by the time you're running line 4,
you're bound to know what b is. Case splitting trees are the efficient
way to compile pattern matching (Augustsson, 1985), testing each
constructor tag at most once. It's an interesting question: can/should
we decouple the implementation of a program we want to run from the
decidable equational theory we want to exploit when reasoning about it.
I can't imagine wanting to run Berry's function, but I can imagine
situtations where those are exactly the laws I need.
Same sort of stuff happens when you define things like simultaneous
substitution by recursion on terms: the identity substitution
is only extensionally the identity function. We can never guarantee to
win this game by crafty choice of computation rules alone (although you
can often do better than you think). Reflection is the way to explain
the art of the possible here.
But the reason Epigram uses eliminators is not that we're especially
attached to the standard elimination constants for inductive datatypes;
it's precisely that we're *not* attached to them. We can program with
*any* induction theorem we can state, and we can even run those programs
if we can prove the induction theorems they rely on. If your notion of
pattern is just based on constructors, you ain't seen nothing. Why not
read 'The view from the left'?
All the best
Conor
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( ( p : P m ! !
! n : Nat ; P : Nat -> * ; mz : P zero ; !--------------------! !
! ! ms m p : P (suc m) ) !
let !------------------------------------------------------------------!
! elim n P mz ms : P n )
elim n P mz ms <= rec n
{ elim n P mz ms <= case n
{ elim zero P mz ms => mz
elim (suc n) P mz ms => ms n (elim n P mz ms)
}
}
------------------------------------------------------------------------------
( x, y : Nat !
let !---------------!
! ack x y : Nat )
ack x y <= elim x
{ ack zero y => suc y
ack (suc m) y <= elim y
{ ack (suc m) zero => ack m (suc zero)
ack (suc m) (suc m') => ack m (ack (suc m) m')
}
}
------------------------------------------------------------------------------
inspect lam n : Nat => ack zero n => (lam n => suc n) : all n : Nat => Nat
------------------------------------------------------------------------------
inspect lam m : Nat => ack (suc m) zero
=> (lam m => ack m (suc zero)) : all m : Nat => Nat
------------------------------------------------------------------------------
inspect lam m, n : Nat => ack (suc m) (suc n)
=>
(lam m ; n => ack m (ack (suc m) n))
: all m : Nat ; n : Nat => Nat
------------------------------------------------------------------------------
( x, y : Nat !
let !-----------------!
! AckType x y : * )
AckType x y => Nat
------------------------------------------------------------------------------
( x, y : Nat !
let !--------------------------!
! ackFun x y : AckType x y )
ackFun x y
=>
elim x (lam x : Nat => all y : Nat => AckType x y) (lam y => suc y)
% (lam m : Nat ; mh : all y : Nat => AckType m y ; y' : Nat!
!=> elim y' (lam y' => AckType (suc m) y') (mh (suc zero)) !
! % (lam m' ; m'h => mh m'h) )
% y
------------------------------------------------------------------------------
let (------------------------------!
! law1 : ackFun zero n = suc n )
law1 => refl
------------------------------------------------------------------------------
let (--------------------------------------------------!
! law2 : ackFun (suc m) zero = ackFun m (suc zero) )
law2 => refl
------------------------------------------------------------------------------
let (---------------------------------------------------------------!
! law3 : ackFun (suc m) (suc m') = ackFun m (ackFun (suc m) m') )
law3 => refl
------------------------------------------------------------------------------
( x, y : Nat ! ( x, y : Nat ; n : Nat !
data !-------------! where !-----------------------!
! ACK x y : * ) ! ret x y n : ACK x y )
------------------------------------------------------------------------------
( c : ACK x y !
let !------------------!
! call x y c : Nat )
call x y c <= case c
{ call x y (ret x y n) => n
}
------------------------------------------------------------------------------
( x, y : Nat !
let !-------------------!
! acktual x y : Nat )
acktual x y
=>
call x y
% (elim x (lam x => all y => ACK x y) (lam y => ret zero y (suc y))!
!% (lam m ; mh ; y' => ! !
! ! elim y' (lam y' => ACK (suc m) y') ! !
! ! % (ret (suc m) zero (call m (suc zero) (mh (suc zero)))) ! !
! ! % (lam m' ; m'h => !! !
! ! ! ret (suc m) (suc m') (call m (call (suc m) m' m'h)!!! !
! ! ! !% (mh (call (suc m) m' m'h))))) !
!% y )
------------------------------------------------------------------------------
inspect lam n => acktual zero n => (lam n => suc n) : all n : Nat => Nat
------------------------------------------------------------------------------
inspect lam m => acktual (suc m) zero
=>
(lam m => !
! call m (suc zero) !
! % (elim m (lam x => all y : Nat => ACK x y) !!
! !% (lam y => ret zero y (suc y)) !!
! !% (lam m' ; mh ; y' => !!!
! ! ! elim y' (lam y'' => ACK (suc m') y'') !!!
! ! ! % (ret (suc m') zero (call m' (suc zero)!!!!!
! ! ! ! !% (mh (suc zero)) ))!!!
! ! ! % (lam m'' ; m'h => ! !!!
! ! ! ! ret (suc m') (suc m'') ! !!!
! ! ! ! % (call m' (call (suc m') m'' m'h)!! !!!
! ! ! ! !% (mh (call (suc m') m'' m'h)) )) )!!
! !% (suc zero) ))
: all m : Nat => Nat
------------------------------------------------------------------------------
inspect lam m ; n => acktual (suc m) (suc n)
=>
(lam m ; n => !
! call m !
! % (call (suc m) n ! !
! !% (elim n (lam y' => ACK (suc m) y') !! !
! ! !% (ret (suc m) zero !!! !
! ! ! !% (call m (suc zero) !!!! !
! ! ! ! !% (elim m (lam x => all y : Nat => ACK x y) !!!!! !
! ! ! ! ! !% (lam y => ret zero y (suc y)) !!!!! !
! ! ! ! ! !% (lam m' ; mh ; y' => !!!!!! !
! ! ! ! ! ! ! elim y' (lam y'' => ACK (suc m') y'')!!!!!! !
! ! ! ! ! ! ! % (ret (suc m') zero ! !!!!!! !
! ! ! ! ! ! ! !% (call m' (suc zero)!! !!!!!! !
! ! ! ! ! ! ! ! !% (mh (suc zero)) )) !!!!!! !
! ! ! ! ! ! ! % (lam m'' ; m'h => ! !!!!!! !
! ! ! ! ! ! ! ! ret (suc m') (suc m'') ! !!!!!! !
! ! ! ! ! ! ! ! % (call m' !! !!!!!! !
! ! ! ! ! ! ! ! !% (call (suc m') m'' m'h) !! !!!!!! !
! ! ! ! ! ! ! ! !% (mh (call (suc m') m''!!!! !!!!!! !
! ! ! ! ! ! ! ! ! ! !% m'h )))) )!!!!! !
! ! ! ! ! !% (suc zero) )))!! !
! ! !% (lam m' ; m'h => ! !! !
! ! ! ! ret (suc m) (suc m') ! !! !
! ! ! ! % (call m (call (suc m) m' m'h) !! !! !
! ! ! ! !% (elim m (lam x => all y : Nat => ACK x y)!!! !! !
! ! ! ! ! !% (lam y => ret zero y (suc y)) !!! !! !
! ! ! ! ! !% (lam m'' ; mh ; y' => ! !!! !! !
! ! ! ! ! ! ! elim y' (lam y'' => ! ! !!! !! !
! ! ! ! ! ! ! ! ACK (suc m'') y'') ! !!! !! !
! ! ! ! ! ! ! % (ret (suc m'') zero ! ! !!! !! !
! ! ! ! ! ! ! !% (call m'' (suc zero)!! ! !!! !! !
! ! ! ! ! ! ! ! !% (mh (suc zero)) )) ! !!! !! !
! ! ! ! ! ! ! % (lam m''' ; m'h' => !! !!! !! !
! ! ! ! ! ! ! ! ret (suc m'') (suc m''') !! !!! !! !
! ! ! ! ! ! ! ! % (call m'' !!! !!! !! !
! ! ! ! ! ! ! ! !% (call (suc m'') m'''!!!! !!! !! !
! ! ! ! ! ! ! ! ! !% m'h' )!!! !!! !! !
! ! ! ! ! ! ! ! !% (mh (call (suc m'')!!!!! !!! !! !
! ! ! ! ! ! ! ! ! ! !% m''' !!!!! !!! !! !
! ! ! ! ! ! ! ! ! ! !% m'h' ))))) !!! !! !
! ! ! ! ! !% (call (suc m) m' m'h) ))) )) !
! % (elim m (lam x => all y : Nat => ACK x y) !!
! !% (lam y => ret zero y (suc y)) !!
! !% (lam m' ; mh ; y' => ! !!
! ! ! elim y' (lam y'' => ACK (suc m') y'') ! !!
! ! ! % (ret (suc m') zero (call m' (suc zero)!!! !!
! ! ! ! !% (mh (suc zero)) ))! !!
! ! ! % (lam m'' ; m'h => ! ! !!
! ! ! ! ret (suc m') (suc m'') ! ! !!
! ! ! ! % (call m' (call (suc m') m'' m'h)!! ! !!
! ! ! ! !% (mh (call (suc m') m'' m'h)) )) ) !!
! !% (call (suc m) n !!!
! ! !% (elim n (lam y' => ACK (suc m) y') !!!!
! ! ! !% (ret (suc m) zero !!!!!
! ! ! ! !% (call m (suc zero) !!!!!!
! ! ! ! ! !% (elim m (lam x => all y : Nat => ACK x y)!!!!!!!
! ! ! ! ! ! !% (lam y => ret zero y (suc y)) !!!!!!!
! ! ! ! ! ! !% (lam m' ; mh ; y' => ! !!!!!!!
! ! ! ! ! ! ! ! elim y' (lam y'' => ! ! !!!!!!!
! ! ! ! ! ! ! ! ! ACK (suc m') y'') ! !!!!!!!
! ! ! ! ! ! ! ! % (ret (suc m') zero ! ! !!!!!!!
! ! ! ! ! ! ! ! !% (call m' (suc zero)!! ! !!!!!!!
! ! ! ! ! ! ! ! ! !% (mh (suc zero)) )) ! !!!!!!!
! ! ! ! ! ! ! ! % (lam m'' ; m'h => !! !!!!!!!
! ! ! ! ! ! ! ! ! ret (suc m') (suc m'') !! !!!!!!!
! ! ! ! ! ! ! ! ! % (call m' !!! !!!!!!!
! ! ! ! ! ! ! ! ! !% (call (suc m') m''! !!! !!!!!!!
! ! ! ! ! ! ! ! ! ! !% m'h ) !!! !!!!!!!
! ! ! ! ! ! ! ! ! !% (mh (call (suc m')!!!!! !!!!!!!
! ! ! ! ! ! ! ! ! ! ! !% m'' !!!!! !!!!!!!
! ! ! ! ! ! ! ! ! ! ! !% m'h ))))) !!!!!!!
! ! ! ! ! ! !% (suc zero) )))!!!!
! ! ! !% (lam m' ; m'h => ! !!!!
! ! ! ! ! ret (suc m) (suc m') ! !!!!
! ! ! ! ! % (call m (call (suc m) m' m'h) !! !!!!
! ! ! ! ! !% (elim m (lam x => ! !!! !!!!
! ! ! ! ! ! ! ! all y : Nat => ACK x y) !!! !!!!
! ! ! ! ! ! !% (lam y => ret zero y (suc y)) !!! !!!!
! ! ! ! ! ! !% (lam m'' ; mh ; y' => !!!! !!!!
! ! ! ! ! ! ! ! elim y' (lam y'' => ! !!!! !!!!
! ! ! ! ! ! ! ! ! ACK (suc m'') y'') !!!! !!!!
! ! ! ! ! ! ! ! % (ret (suc m'') zero ! !!!! !!!!
! ! ! ! ! ! ! ! !% (call m'' (suc zero)!! !!!! !!!!
! ! ! ! ! ! ! ! ! !% (mh (suc zero)) )) !!!! !!!!
! ! ! ! ! ! ! ! % (lam m''' ; m'h' => !!!!! !!!!
! ! ! ! ! ! ! ! ! ret (suc m'') (suc m''')!!!!! !!!!
! ! ! ! ! ! ! ! ! % (call m'' !!!!!! !!!!
! ! ! ! ! ! ! ! ! !% (call (suc m'')! !!!!!! !!!!
! ! ! ! ! ! ! ! ! ! !% m''' ! !!!!!! !!!!
! ! ! ! ! ! ! ! ! ! !% m'h' ) !!!!!! !!!!
! ! ! ! ! ! ! ! ! !% (mh (call !!!!!!!! !!!!
! ! ! ! ! ! ! ! ! ! ! !% (suc m'')!!!!!!!! !!!!
! ! ! ! ! ! ! ! ! ! ! !% m''' !!!!!!!! !!!!
! ! ! ! ! ! ! ! ! ! ! !% m'h' )))))!!! !!!!
! ! ! ! ! ! !% (call (suc m) m' m'h) ))) ))))
: all m : Nat ; n : Nat => Nat
------------------------------------------------------------------------------
