Japanese version
A definition, like function application is left-associative, is alike a rule of a sport. One of the rules of basketball is a player with the ball must dribble a ball when the player moves. Why is it? Because it is a rule of the game. If someone dribbles a ball in baseball, it does not make any sense (in case baseball makes sense). If a soccer player uses hands except the goal-keeper, it is a foul. Why is it so even they all use a ball? That is out of question. It is the rules of the game. Mathematics also has the similar aspect. ``Why is it left-associative?'' ``Because it is a definition. (means that's the rule.)''
Unfortunate starts when someone teaches this mathematical rule is the unique and unalterable truth. If one believe 1+1=2 is the unique and unalterable truth, then s/he could not understand mathematics at some point. For example, there is a mathematics 1+1=1. This mathematics is used in nowadays computer. Nowadays computer widely uses binary system, and binary system has only `0' and `1.' Then 1+1=2 could not be possible if 2 does not exist in one digits computation. Another unfortunate could be someone think now 1+1=2 is a mistake. Like there are rules for baseball and football, each game has each rule/truth. 1+1=2 is useful, many cases it is considered truth, but, it is done after it has been defined. Namely, if the rules of a game are defined, that rules become the unique and unalterable truth/rule/definition.
Both in sports and mathematics, we are always interested in a similar aspects. ``Does the rule/definition make an interesting game?'' I think we do not so much care about the rule or the definition itself. I am much interested in the game, not the rules. If we define an operation of addition, does it lead something interesting? If we think about a system which only uses addition and multiplication, what will it be? By the way, the system of linear algebra consists of addition and one constant multiplication.
When I think about other people, I usually found more interesting about ``What this person did?'' than ``Who is this person? (weight, hight, outlook, name, ...)'' I also find that ``what is the function of the definition?'' is more intriguing than the definition itself. I happen to have a question ``Why we need this definition?'' for many times. Then I hate mathematics at the moment. But, I think I should not have this question.
``But Marvin, no mathematics teacher taught me such things. Do you know why?''
``Because it is obvious.''
If someone understand well, then they did not realized it. Even they did not cast a question. However, I always feel no question is not a good sign.
Let's see the SUCC function again.
SUCC := λn f x. f (n f x)
This is a short form of
SUCC := ((λn. λf). λx). f (n f x).
The left side of ``.'' indicates function, we could remove two redundant λs out of three λs. More precisely, this is related with ``curring.'' ``Curring'' coined after Haskell Curry, but it seems Curry is not the inventor (Moses Schoenfinkel and Gottlob Frege). It is the technique of transforming a multiple arguments function to a combination of single argument functions. If you fix all arguments except the first one, you get a function of the non-first arguments in this technique. This means we only need to think about single argument function. Why do we think about curring? Because single argument function is simpler than multiple argument function. If the effects are the same, (lazy) mathematician likes the simpler one.
A definition, like function application is left-associative, is alike a rule of a sport. One of the rules of basketball is a player with the ball must dribble a ball when the player moves. Why is it? Because it is a rule of the game. If someone dribbles a ball in baseball, it does not make any sense (in case baseball makes sense). If a soccer player uses hands except the goal-keeper, it is a foul. Why is it so even they all use a ball? That is out of question. It is the rules of the game. Mathematics also has the similar aspect. ``Why is it left-associative?'' ``Because it is a definition. (means that's the rule.)''
Unfortunate starts when someone teaches this mathematical rule is the unique and unalterable truth. If one believe 1+1=2 is the unique and unalterable truth, then s/he could not understand mathematics at some point. For example, there is a mathematics 1+1=1. This mathematics is used in nowadays computer. Nowadays computer widely uses binary system, and binary system has only `0' and `1.' Then 1+1=2 could not be possible if 2 does not exist in one digits computation. Another unfortunate could be someone think now 1+1=2 is a mistake. Like there are rules for baseball and football, each game has each rule/truth. 1+1=2 is useful, many cases it is considered truth, but, it is done after it has been defined. Namely, if the rules of a game are defined, that rules become the unique and unalterable truth/rule/definition.
Both in sports and mathematics, we are always interested in a similar aspects. ``Does the rule/definition make an interesting game?'' I think we do not so much care about the rule or the definition itself. I am much interested in the game, not the rules. If we define an operation of addition, does it lead something interesting? If we think about a system which only uses addition and multiplication, what will it be? By the way, the system of linear algebra consists of addition and one constant multiplication.
When I think about other people, I usually found more interesting about ``What this person did?'' than ``Who is this person? (weight, hight, outlook, name, ...)'' I also find that ``what is the function of the definition?'' is more intriguing than the definition itself. I happen to have a question ``Why we need this definition?'' for many times. Then I hate mathematics at the moment. But, I think I should not have this question.
``But Marvin, no mathematics teacher taught me such things. Do you know why?''
``Because it is obvious.''
If someone understand well, then they did not realized it. Even they did not cast a question. However, I always feel no question is not a good sign.
Let's see the SUCC function again.
SUCC := λn f x. f (n f x)
This is a short form of
SUCC := ((λn. λf). λx). f (n f x).
The left side of ``.'' indicates function, we could remove two redundant λs out of three λs. More precisely, this is related with ``curring.'' ``Curring'' coined after Haskell Curry, but it seems Curry is not the inventor (Moses Schoenfinkel and Gottlob Frege). It is the technique of transforming a multiple arguments function to a combination of single argument functions. If you fix all arguments except the first one, you get a function of the non-first arguments in this technique. This means we only need to think about single argument function. Why do we think about curring? Because single argument function is simpler than multiple argument function. If the effects are the same, (lazy) mathematician likes the simpler one.
Comments