Type Theory exploration
Type Theory
My understanding of Type theory.
Defining natural numbers:
zero:Nat
succ(n:Nat):Nat
So for example defining the number 2:
succ(succ(zero)):Nat
same as???
isNat(zero)
ForAll(n) : isNat(n)=>isNat(succ(n))
We can define operations like plus and times and equals
//define proofs that n==n
equals(zero,zero):Equals<zero,zero>
equals(succ(n:Nat),succ(n:Nat)):Equals<succ(n:Nat),succ(n:Nat)>
Proofs and Dependent types
Define a dependent type Even<n:Nat> which is a proof that n is even.
{a:Nat, p:Equals<times(2,a),n>}:Even<n:Nat>
So that for example the following is a proof that 6 is even:
{3, equals(times(2,3),6)}:Even<6>
which becomes {3:Nat,equals(6,6):Equals<6,6>} :Even<6>
{a:Nat , p:Equals<times(2,a),n>}:Even<n:Nat>
isEven(n) = n => (a => (isNat(a) & equals(times(2,a),n)))
isEven(6) (3)
In C syntax
typedef Even<Nat n> { Nat a, Equals<times(2,a),n> p };
Why not (?):
{a:Nat, p:IsTrue<equals(times(2,a),n)>}:Even<n:Nat>
{3,proof}:Even<6>
isEven( isNat(a) , equals(times(2,a),n) , n)
larger(0,1):LargerThan<0,1>
larger(n,succ(n)):LargerThan<n,succ(n)>
larger(succ(n),succ(n)):LargerThan<succ(n),succ(n)>
{a:Nat, b:Nat, p1:LargerThan<1,a>,p2:LargerThan<1,b>, p3:Equals<times(a,b),n>}: Composite<n:Nat>
Proof:
{2,3,larger(1,2),larger(1,3),equals(times(2,3),6)}:Composite<6>
isComposite = n->(a->b-> a & b & isLarger(1,a) & isLarger(1,b) & a*b=n)
f(x:Nat, p1:isComposite<n> ):G
(isNat(x) && isComposite(x)(a)(b) ==> isG(x))
proof:IsTrue<true>
{a:Nat, b:Nat, p1:IsTrue<larger(1,a)>,p2:IsTrue<larger(1,b)>, p3:IsTrue<equals(times(a,b),n)>}: Composite<n:Nat>
Proof 1+1=2
sum(a:Nat,b:Nat):Sum<a,b>
zero_plus(n:Nat):Equals<Sum<zero,n>,n>
:Equals<x:Sum<a,b>,c:Nat>
Equals
isNat(a) & isNat(b) & larger(1,a) & larger(1,b) & equals(a*b,n) => isComposite(c)
{a:Nat-> b:Nat -> c: Nat -> n:Nat -> a^n+b^n=c^n }:FermatLastTheorem
FermatLastTheorem = (a,b,c,n)=>(a^n+b^n=c^n)
Comments
Post a Comment