Earlier, we saw that function application is written by putting the parameter after the function term. So, if we want to call the above function with the parameter "5" of type "nat", we write: (λ x : nat . (add x x)) 5 : nat The lambda term was type "nat nat", which meant that given a "nat" as an argument, it will produce a term of type "nat". Since we have given it the argument "5", the above term has type "nat". Reduction works by substituting the argument "5" for the parameter "x" in the term "(add x x)", so the term computes to: (add 5 5) : nat which obviously computes to 10 : nat A lambda term is often called an "anonymous function" because it has no name. Often, to make things easier to read, a name is given to a lambda term. This is merely a notation and has no mathematical meaning. Some authors call it "notational equality". A name might be given to the function above using the notation: double : nat nat ::= (λ x : nat . (add x x)) This is the same function as above, just a different way to write it. So the term double 5 : nat still computes to 10 : nat Dependent typing Dependent typing is when the type returned by a function depends on the value of its argument. For example, when a type theory has a rule that defines the type "bool", it also defines the function "if". The function "if" takes 3 arguments and "if true b c" computes to "b" and "if false b c" computes to "c". But what is the type of "if a b c"? If "b" and "c" have the same type, it is obvious: "if a b c" has the same type as "b" and "c". Thus, assuming "a : bool", if a 2 4 : nat if a false true : bool But if "b" and "c" have different types, then the type of "if a b c" depends on the value of "a". We use the symbol "Π" to indicate a function that takes an argument and returns a type. Assuming we have some types "B" and C" and "a : bool", "b : B" and "c : C", then if a b c : (Π a : bool . B C if a B C)