Jonte Deakin year 12 semester 2 IT assignment

Ok, So I have calmed down from last weeks post. I thought about it and it wasn't as cool as I initially hoped, but I think it's still an idea worth pursuing. I did start pursuing it and read a lot about lots of different things. I have come to the conclusion that it's probably a form of dependent typing. I have not yet found the idea replicated anywhere but I am definitely thinking it's probably some weird subset of a pre-existing theory. I think it is also probably related to recursive typing. One last thing is that it appears to not really hold all that much extra power in the realms of normal typing algorithms, but I have had fun with it. The overall summary (just in case last weeks post was a bit too scatterbrained) is that I think we could enhance simply typed lambda calculus where instead of having variables (a -> a, a is the variable) in the type, we can create a way of describing acceptable inputs to the function. We can do this using context-free grammar (cf...

 Ok so I read through the original paper on total functional programming and had a great time. Although it ended up not telling em about primtive recursion (a little bit but not enough to write into my language) and the most significant thing was that it linked back to the original hilbert recursion paper.  I haven't read the hilber recursion paper as of yet because I have had enormous problems getting my hands on it. It's on springerlink and springerlink is busted and I can't pirate it because it's not well known enough to pirate.  Though after intense frustration that my one good lead led back to the same paper, I asked my sister for help and she showed me how to get it ezpz through google scholar. I then started reading the paper and got a little bored (it's very densely written) so I started daydreaming about the potential type system I might have. This led to a series of very fun and interesting ideas that I am too excited about to finish the primitive recursio...

 This week I was reading a bit about maths and other things and discovered that my approach to primitive recursion has already been done. It is called structural recursion https://en.wikipedia.org/wiki/Structural_induction. (this is about my definition of primitive recursion, not the integration. Also as a side note, I am using primitive recursion in place of terminating recursion because I am lazy with my terminology, I apologize). I also realized that my project wasn't that interesting and that my type system especially was kinda lame. I feel as if I can go harder and make my type system more interesting and worth doing. I also feel that the amount of time I've given myself too much time so I'll end up not really doing much for most of it. Due to these reasons, I have been exploring some type theories to see if there's anything I can mangle into a type system for this assignment.  The main candidates (so far, this is early days of research) are: - Hindley Milner ...

I did a little bit of commenting and added a tutorial to make the project suitable to submit. During this I discovered a problem with my defininition of primitive functions, but it is too late to fix before the prototype is due. I am planning to update the defintion to probably just be the primitive functions, although I am considering two alternatives, substructural or hilbert recursion. I then submitted the project and will do no further work for a few weeks while I catch up on other assignments. note: I did miss last weeks blog post and probably did the work listed above then, it's hard to remember, it's been very hectic. Sorry I'll try to stick closer to the one post a week format from now on.