Commit 357cf141 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

McCarthy

parent 33b85eba
(; Les Types ;)
Nat : Type.
Bool : Type.
(; Constructeurs ;)
0 : Nat.
S : Nat -> Nat.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
def 5 := S 4.
def 6 := S 5.
def 7 := S 6.
def 8 := S 7.
def 9 := S 8.
def 10 := S 9.
def 11 := S 10.
def 12 := S 11.
def 13 := S 12.
def 14 := S 13.
def 15 := S 14.
def 16 := S 15.
def 17 := S 16.
def 18 := S 17.
def 19 := S 18.
def 20 := S 19.
def 21 := S 20.
def 22 := S 21.
def 23 := S 22.
def 24 := S 23.
def 25 := S 24.
def 26 := S 25.
def 27 := S 26.
def 28 := S 27.
def 29 := S 28.
def 30 := S 29.
def 31 := S 30.
def 32 := S 31.
def 33 := S 32.
def 34 := S 33.
def 35 := S 34.
def 36 := S 35.
def 37 := S 36.
def 38 := S 37.
def 39 := S 38.
def 40 := S 39.
def 41 := S 40.
def 42 := S 41.
def 43 := S 42.
def 44 := S 43.
def 45 := S 44.
def 46 := S 45.
def 47 := S 46.
def 48 := S 47.
def 49 := S 48.
def 50 := S 49.
def 51 := S 50.
def 52 := S 51.
def 53 := S 52.
def 54 := S 53.
def 55 := S 54.
def 56 := S 55.
def 57 := S 56.
def 58 := S 57.
def 59 := S 58.
def 60 := S 59.
def 61 := S 60.
def 62 := S 61.
def 63 := S 62.
def 64 := S 63.
def 65 := S 64.
def 66 := S 65.
def 67 := S 66.
def 68 := S 67.
def 69 := S 68.
def 70 := S 69.
def 71 := S 70.
def 72 := S 71.
def 73 := S 72.
def 74 := S 73.
def 75 := S 74.
def 76 := S 75.
def 77 := S 76.
def 78 := S 77.
def 79 := S 78.
def 80 := S 79.
def 81 := S 80.
def 82 := S 81.
def 83 := S 82.
def 84 := S 83.
def 85 := S 84.
def 86 := S 85.
def 87 := S 86.
def 88 := S 87.
def 89 := S 88.
def 90 := S 89.
def 91 := S 90.
def 92 := S 91.
def 93 := S 92.
def 94 := S 93.
def 95 := S 94.
def 96 := S 95.
def 97 := S 96.
def 98 := S 97.
def 99 := S 98.
def 100 := S 99.
True : Bool.
False : Bool.
(; Les fonctions ;)
def plus : Nat -> Nat -> Nat.
[n] plus 0 n --> n
[m, n] plus (S m) n --> S (plus m n)
[n] plus n 0 --> n
[m, n] plus m (S n) --> S (plus m n).
def leq : Nat -> Nat -> Bool.
[] leq 0 _ --> True
[m] leq (S m) 0 --> False
[m, n] leq (S m) (S n) --> leq m n.
def moins : Nat -> Nat -> Nat.
[x] moins x 0 --> x.
[x,y] moins (S x) (S y) --> moins x y.
def McCarthy : Nat -> Nat.
def MC_aux : Nat -> Bool -> Nat.
[x] McCarthy x --> MC_aux x (leq x 100).
[x] MC_aux x True --> McCarthy (McCarthy (plus x 11)).
[x] MC_aux x False --> moins x 10.
#EVAL McCarthy 81.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment