-
Notifications
You must be signed in to change notification settings - Fork 2
/
gcd.typ
70 lines (60 loc) · 1.23 KB
/
gcd.typ
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
type NS(α) = μα X [Z | S of X]
type N = NS(∞)
val rec sub : ∀α∀β (NS(β+1) → [S of NS(α)] → [ I of NS(α) | P of NS(β) ]) =
fun n m →
case m of
| S m' →
(case m' of
| Z →
(case n of
| Z → I Z
| S n' → P n')
| S m'' →
(case n of
| Z → I Z
| S n' →
(case sub n' (S m'') of
| I r → I (S r)
| P d → P d)))
eval sub Z (S Z)
eval sub (S Z) (S Z)
eval sub (S (S Z)) (S Z)
eval sub Z (S (S Z))
eval sub (S Z) (S (S Z))
eval sub (S (S Z)) (S (S Z))
eval sub (S (S (S Z))) (S (S Z))
val rec mod : ∀α∀β NS(β+1) → [S of NS(α+1)] → NS(α+1) =
fun n m →
case sub n m of
| I r → r
| P n' →
(case n' of
| Z → Z
| S n'' → mod (S n'') m)
val rec gcd : N → N → N = fun n m →
case n of
| Z → m
| S n' →
(case n' of
| Z → S Z
| S n'' →
(case m of
| Z → n
| S m' →
gcd (mod (S m') (S (S n''))) (S (S n''))))
val 0 = Z
val 1 = S 0
val 2 = S 1
val 3 = S 2
val 4 = S 3
val 5 = S 4
val 6 = S 5
val 7 = S 6
val 8 = S 7
val 9 = S 8
val 10 = S 9
val 11 = S 10
val 12 = S 11
val 13 = S 12
eval gcd 9 12
eval gcd 12 9