Comment by auggierose
2 years ago
> Anyway the point here is that we want to formulate a theory with the lowest amount of primitives and axiomatic concepts.
A theory makes only sense with respect to some logic. So first, you need to define what logic you are using. This logic is your theory with the lowest amount of primitives and axiomatic concepts.
Now, once you have that, you can turn your attention to other things on top of that. If you are interested in functions only, sure. You can for example study the lambda calculus.
But don't pretend that this is so that you can reason about computer programs better. Sure, learning more about functions is useful, but numbers are also very important for computer programs. So are trees. And graphs. Expressing all of these just in terms of functions can be a fun exercise (pun intended, Church numerals anyone?). But instead of trying to express the important concepts of your program as functions, and then studying them, maybe your time is better spent studying the concepts themselves directly.
>A theory makes only sense with respect to some logic. So first, you need to define what logic you are using. This logic is your theory with the lowest amount of primitives and axiomatic concepts.
Logic as I know it can't be made up. It's already well defined and the basis for all other formal theories.
The lowest amount of primitives and axiomatic concepts is largely a design choice for developing a theory. Makes it easier to deal with the theory rather than a theory that starts out with extremely complicated axioms.
>But don't pretend that this is so that you can reason about computer programs better. Sure, learning more about functions is useful, but numbers are also very important for computer programs. So are trees. And graphs. Expressing all of these just in terms of functions can be a fun exercise (pun intended, Church numerals anyone?). But instead of trying to express the important concepts of your program as functions, and then studying them, maybe your time is better spent studying the concepts themselves directly.
Yeah but I would want to prune all that other stuff away and focus on a theory on the best way to organize and abstract programs. The primitive most important for that is the function because that's basically at it's core all a computer does, just calculate stuff.
> Logic as I know it can't be made up. It's already well defined and the basis for all other formal theories.
Of course logic can be made up, and in fact, all logics are. First-order logic, simply-typed higher order logic, dependent type theory, all made up.
My favourite made up logic is Abstraction Logic (http://abstractionlogic.com).
But I guess what you mean is that you are a mathematical realist. That's good! I am too.
> Yeah but I would want to prune all that other stuff away and focus on a theory on the best way to organize and abstract programs. The primitive most important for that is the function because that's basically at it's core all a computer does, just calculate stuff.
If that's what you want to do, then that's what you want to do!
>Of course logic can be made up, and in fact, all logics are. First-order logic, simply-typed higher order logic, dependent type theory, all made up.
That's like saying math is made up. Is it made up or is it discovered?
You're just being pedantic.
>If that's what you want to do, then that's what you want to do!
Yeah and if you want some theory of program design that encompasses every damn concept under the sun as an axiom go for it as well! Genius!
2 replies →