This entire project is based upon the book, “Type Theory and Formal Proof: An Introduction”, by Nederpelt & Geuvers. I’m not quite sure at the initial writing of this how it’ll all work out, but at least one goal is to turn this into an introduction to Computer Science, and another is to write a proof assistant.
For answers to selected exercises in the book, see Answers.
Rob Nederpelt Herman Geuvers CoRN
This combination helps you navigate to find a file.
This combination evaluates the preceding S-Expression.
(org-toggle-pretty-entries) This one makes LaTeX symbols show up using the UTF-8 character instead of the symbol alias.
This one toggles paredit mode, which is a minor mode for Emacs for navigating parenthetical expressions. Paredit Mode is a blog article that should help you get started.
Imagine a function as a box. You give the box your input(s), and it spits out your output(s). Each set of inputs corresponds with only one output. This means that every time you throw identical inputs into the box, you can expect it to spit out the same output. You can choose to think about it in some other way if it suits you better. That being said, here are five examples of the function-box:
We’re going to start with the most basic function you can have.
λx.x
(λx.x)(1)
(λx.x)(2)
(λx.x)(3)
(fn [x] x)
((fn [x] x) 1)
((fn [x] x) 2)
((fn [x] x) 3)
(x) => x
((x) => x)(1)
((x) => x)(2)
((x) => x)(3)\x -> x
(\x -> x) 1
(\x -> x) 2
(\x -> x) 3
fn (x) -> x end
(fn (x) -> x end).(1)
(fn (x) -> x end).(2)
(fn (x) -> x end).(3)lambda x : x
(lambda x : x)(1)
(lambda x : x)(2)
(lambda x : x)(3)// This is not untyped, as Java requires a return type for functions
Function<Integer, Integer> identity = (x) -> x;
identity.apply(1);
identity.apply(2);
identity.apply(3);[](auto x) { return x; }
([](auto x) { return x; })(1);
([](auto x) { return x; })(2);
([](auto x) { return x; })(3);// This is not untyped, as C# requires a return type for functions
Func<int, int> identity = (x) => x;
identity(1);
identity(2);
identity(3);fun x -> x
(fun x -> x) 1
(fun x -> x) 2
(fun x -> x) 3
(lambda (x) x)
((lambda (x) x) 1)
((lambda (x) x) 2)
((lambda (x) x) 3)
// Kotlin can't do type inference in this context, so we need to give x a type.
{ x: Int -> x }
{ x: Int -> x }(1)
{ x: Int -> x }(2)
{ x: Int -> x }(3)
let identity = |x| { x };
identity(1);
identity(2);
identity(3);λx.x + x
(λx.x + x)(1)
(λx.x + x)(2)
(λx.x + x)(3)
(fn [x] (+ x x))
((fn [x] (+ x x)) 1)
((fn [x] (+ x x)) 2)
((fn [x] (+ x x)) 3)
(x) => (x + x)
((x) => (x + x))(1)
((x) => (x + x))(2)
((x) => (x + x))(3)\x -> x + x
(\x -> x + x) 1
(\x -> x + x) 2
(\x -> x + x) 3
(fn (x) -> x + x end)
(fn (x) -> x + x end).(1)
(fn (x) -> x + x end).(2)
(fn (x) -> x + x end).(3)lambda x : x + x
(lambda x : x + x)(1)
(lambda x : x + x)(2)
(lambda x : x + x)(3)// This is not untyped, as Java requires a return type for functions
Function<Integer, Integer> doubling = (x) -> x + x;
doubling.apply(1);
doubling.apply(2);
doubling.apply(3);[](auto x) { return x + x; };
([](auto x) { return x + x; })(1);
([](auto x) { return x + x; })(2);
([](auto x) { return x + x; })(3);// This is not untyped, as C# requires a return type for functions
Func<int, int> doubling = (x) => x + x;
doubling(1);
doubling(2);
doubling(3);fun x -> x + x
(fun x -> x + x) 1
(fun x -> x + x) 2
(fun x -> x + x) 3
(lambda (x) (+ x x))
((lambda (x) (+ x x)) 1)
((lambda (x) (+ x x)) 2)
((lambda (x) (+ x x)) 3)
// Kotlin can't do type inference in this context, so we need to give x a type.
{ x: Int -> x + x}
{ x: Int -> x + x } (1)
{ x: Int -> x + x } (2)
{ x: Int -> x + x } (3)
let doubling = |x| { x + x };
doubling(1);
doubling(2);
doubling(3);λx.x² + 1
(λx.x² + 1)(1)
(λx.x² + 1)(2)
(λx.x² + 1)(3)
(fn [x] (+ (* x x) 1))
((fn [x] (+ (* x x) 1)) 1)
((fn [x] (+ (* x x) 1)) 2)
((fn [x] (+ (* x x) 1)) 3)
(x) => (x * x) + 1
((x) => (x * x) + 1)(1)
((x) => (x * x) + 1)(2)
((x) => (x * x) + 1)(3)\x -> (x * x) + 1
(\x -> (x * x) + 1) 1
(\x -> (x * x) + 1) 2
(\x -> (x * x) + 1) 3
(fn (x) -> (x * x) + 1 end)
(fn (x) -> (x * x) + 1 end).(1)
(fn (x) -> (x * x) + 1 end).(2)
(fn (x) -> (x * x) + 1 end).(3)lambda x : (x * x) + 1
(lambda x : (x * x) + 1)(1)
(lambda x : (x * x) + 1)(2)
(lambda x : (x * x) + 1)(3)// This is not untyped, as Java requires a return type for functions
Function<Integer, Integer> squarePlusOne = (x) -> (x * x) + 1;
squarePlusOne.apply(1);
squarePlusOne.apply(2);
squarePlusOne.apply(3);[](auto x) { return (x * x) + 1; };
([](auto x) { return (x * x) + 1; }(1));
([](auto x) { return (x * x) + 1; }(2));
([](auto x) { return (x * x) + 1; }(3));// This is not untyped, as C# requires a return type for functions
Func<int, int> squarePlusOne = (x) => (x * x) + 1;
squarePlusOne(1);
squarePlusOne(2);
squarePlusOne(3);fun x -> x * x + 1
(fun x -> x * x + 1) 1
(fun x -> x * x + 1) 2
(fun x -> x * x + 1) 3
(lambda (x) (+ (* x x) 1))
((lambda (x) (+ (* x x) 1)) 1)
((lambda (x) (+ (* x x) 1)) 2)
((lambda (x) (+ (* x x) 1)) 3)
// Kotlin can't do type inference in this context, so we need to give x a type.
{ x: Int -> (x * x) + 1}
{ x: Int -> (x * x) + 1}(1)
{ x: Int -> (x * x) + 1}(2)
{ x: Int -> (x * x) + 1}(3)
let square_plus_one = |x| { x * x + 1 };
square_plus_one(1);
square_plus_one(2);
square_plus_one(3);λx.5
(λx.5)(1)
(λx.5)(2)
(λx.5)(3)
(fn [x] 5)
((fn [x] 5) 1)
((fn [x] 5) 2)
((fn [x] 5) 3)
(x) => 5
((x) => 5)(1)
((x) => 5)(2)
((x) => 5)(3)\x -> 5
(\x -> 5) 1
(\x -> 5) 2
(\x -> 5) 3
Standard convention is to prefix the names of arguments which will not be used with ‘_’, in Elixir
(fn (_x) -> 5 end)
(fn (_x) -> 5 end).(1)
(fn (_x) -> 5 end).(2)
(fn (_x) -> 5 end).(3)lambda x : 5
(lambda x : 5)(1)
(lambda x : 5)(2)
(lambda x : 5)(3)// This is not untyped, as Java requires a return type for functions
Function<Integer, Integer> returnConstant = (x) -> 5;
returnConstant.apply(1);
returnConstant.apply(2);
returnConstant.apply(3);[](auto x) { return 5 };
([](auto x) { return 5; }(1));
([](auto x) { return 5; }(2));
([](auto x) { return 5; }(3));// This is not untyped, as C# requires a return type for functions
Func<int, int> returnConstant = (x) => 5;
returnConstant(1);
returnConstant(2);
returnConstant(3);fun x -> 5
(fun x -> 5) 1
(fun x -> 5) 2
(fun x -> 5) 3
(lambda (x) 5)
((lambda (x) 5) 1)
((lambda (x) 5) 2)
((lambda (x) 5) 3)
// Kotlin can't do type inference in this context, so we need to give x a type.
{ x: Int -> 5}
{ x: Int -> 5}(1)
{ x: Int -> 5}(2)
{ x: Int -> 5}(3)
let return_constant = |x| { 5 };
return_constant(1);
return_constant(2);
return_constant(3);λx.(λy.x + y)
(λx.(λy.x + y))(1)
(λx.(λy.x + y))(2)
(λx.(λy.x + y))(3)
(fn [x] (fn [y] (+ x y)))
((fn [x] (fn [y] (+ x y))) 1)
((fn [x] (fn [y] (+ x y))) 2)
((fn [x] (fn [y] (+ x y))) 3)
(x) => ((y) => x + y)
((x) => ((y) => x + y))(1)
((x) => ((y) => x + y))(2)
((x) => ((y) => x + y))(3)\x -> (\y -> x + y)
(\x -> (\y -> x + y)) 1
(\x -> (\y -> x + y)) 2
(\x -> (\y -> x + y)) 3
(fn (x) -> (fn (y) -> x + y end) end)
(fn (x) -> (fn (y) -> x + y end) end).(1)
(fn (x) -> (fn (y) -> x + y end) end).(2)
(fn (x) -> (fn (y) -> x + y end) end).(3)lambda x : (lambda y : x + y)
(lambda x : (lambda y : x + y))(1)
(lambda x : (lambda y : x + y))(2)
(lambda x : (lambda y : x + y))(3)// This is not untyped, as Java requires a return type for functions
Function<Integer, Function<Integer, Integer>> makeAdder = (x) -> ((y) -> (x + y));
var add1 = makeAdder.apply(1);
var add2 = makeAdder.apply(2);
var add3 = makeAdder.apply(3);[](auto x) { return [x](auto y) { return x + y; }; };
auto add1 = ([](auto x) { return [x](auto y) { return x + y; }; }(1));
auto add2 = ([](auto x) { return [x](auto y) { return x + y; }; }(2));
auto add3 = ([](auto x) { return [x](auto y) { return x + y; }; }(3));// This is not untyped, as C# requires a return type for functions
Func<int, Func<int, int>> makeAdder = (x) => ((y) => x + y);
var add1 = makeAdder(1);
var add2 = makeAdder(2);
var add3 = makeAdder(3);fun x -> (fun y -> x + y)
(fun x -> (fun y -> x + y)) 1
(fun x -> (fun y -> x + y)) 2
(fun x -> (fun y -> x + y)) 3
(lambda (x) (lambda (y) (+ x y)))
((lambda (x) (lambda (y) (+ x y))) 1)
((lambda (x) (lambda (y) (+ x y))) 2)
((lambda (x) (lambda (y) (+ x y))) 3)
// Kotlin can't do type inference in this context, so we need to give x a type.
{ x: Int -> { y: Int -> x + y}}
{ x: Int -> { y: Int -> x + y}} (1)
{ x: Int -> { y: Int -> x + y}} (2)
{ x: Int -> { y: Int -> x + y}} (3)
//Rust can infer the types of the values passed into functions, but must have types of unassigned parameters explicitly defined in the declaration of the function.
let make_adder = |x| { move |y: i32| { x + y } };
let add1 = make_adder(1);
let add2 = make_adder(2);
let add3 = make_adder(3);A function from a set X to a set Y is an assignment of an element of Y to each element of X. The set X is called the domain of the function and the set Y is called the codomain of the function.
A function, its domain, and its codomain, are declared by the notation f: X->Y, and the value of a function f at an element x of X, denoted by f(x), is called the image of x under f, or the value of f applied to the argument x.