> Conor McBride wrote: > Yong Luo wrote: > > >>Primitive recursion + function types give you all functions provable > >>total in Arithmetic, Goedel proved this (that's where System T comes > >>from). > >> > >> > >> > > > >Hello, Thorsten, > > > >In practice, it is sometimes not easy to change a non-primitive recursion > >to > >a primitive one. > >Here is another example which is similar to the Ackermann function. > > > >f 0 n = S n > >f (S 0) n = S (S n) > >f (S (S m)) 0 = f m (S 0) > >f (S (S m)) (S n) = > > f (S m) (f m n) + > > f m (f (S m) n) + > > f m (f (S m) (S n)) + > > f (S m) (f (S (S m)) n) > > > > > > Did you check this example in Epigram? > > Conor
Somehow the question wether a recursion is applicable in dependent type theory as is tastes like a Jump & Run: jump over at least one constructor on your way from the left to the right and run the function on what's left (on the right). And you can green the left like hell with with derived and motivated eliminations. But since we all know by now, that not all patterns can be reached by this techniques, we shouldn't underestimate taxonomies of the left. At least for informative error messages, when something like maj is supplied in batch mode. Yong insisted, type theory should be more liberal to what one is likely (standard ack) (not likes, that's Thorstens) to scribble down and allow patterns without a 'sweet spot' (as in majority). But when you start to mention partial functions, you're not far from having to specify your design against overlapping patterns as these then will raise priority (i.e. fairness) issues between your equations. And i think, ever since the SPJ book, it's partial functions which are the main reason for the linearity requirement of patterns in todays functional programming languages. Spotting inductive positions (this time i do not mean the position of an inductive argument of a type constructor) in patterns can be an issue of ever being able to compute results in presence of partial functions (Yong) or efficiency, when abducting from the image of a function (Conor). Cheers, Sebastian
