Its been a long time since i last touched this probably because I had been writing elsewhere. That and stress. But the technical stuff I should really be writing in my notes a second draft, and i should probably write about less technical stuff and more intuitive things as well.
Anyway I should use this post to sum up some general feelings I have had from my general studies this summer that I haven't yet noted.
It has come to my attention that the single system of notation for logic and math may be damaging. Even from a psycholinguistic viewpoint, if one accepts the mild version of the whorf-sapir hypothesis then it is easy to conclude that multiple syntaxes for representing things would be important. One such example is the difference between explicit and ordered based role assignment. Current mathematical notation is based on the idea that arguments to functions are passed into it in a certain order and we determine the role of the arguments play in the function by matching them to variables which are also ordered. Example:
F(x,y) = x-y.
We can reason here saying "4 is the first thing so I will replace it with the first variable in the definition (x). 3 is the second so I will replace it with second variable in the definition (y)."
Now this system is intutive and easy. It has served us well. But if we look at language as a structure we find a much different mechanism. Broadly speaking language marks the arguments role in the function/predicate. This doesn't seem to be recognized as much as it should by semanticisits using logic and is pretty rare. As far as I know the only instance of it i can find in math and compsci is in ocaml where labeled roles are allowed for functions. An example is below.
F(x,y) = x/y
F(y:3 , x:6)
We evaluate here by saying oh were supposed to replace y with 3 and x with 6 and we get 2. Here we have labeled 3 and 6 with their respective "roles" in the function.
Now both of these systems are equivalent right? Both are just as good.. but if you think about it more closely, having the roles marked allows us much more flexibility. Take partial applications in lambda calculus.
Let subtract = fun xy.x-y;
If we wish to write a function that tells you what you get when you stubtract three from something we only need to write
Let 3minus = subtract 3;
However if we want to see what happens when we take something and stubtract three from it, writing that function out becomes a bit more of a hassel
let subtractfrom3 = fun a. subtract a 3;
This is plan stupid. If we used marked roles the function becomes simpler to write.
let subtractfrom3 = subtract b:3 ;
let 3minus = subtract a:3;
(instead of using a and b we could simply mark it with 1,2,3..)
more fun uses of role-marking later