Commit dd9ab2f9 authored by Gaspard Ferey's avatar Gaspard Ferey

merge

parents 0bd83659 69b4bd15
#NAME cc.
(; Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
Maude joins all critical pairs.
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels (where k *closed* Sort) from 0 or 1 level from 0.
Can only lift k levels from 0 or 1 level from universe i.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
......
load cc.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
......@@ -9,7 +9,7 @@ This variant implements :
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels (where k *closed* Sort) from 0 or 1 level from 0.
Can only lift k levels from 0 or 1 level from universe i.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
......
......@@ -13,7 +13,7 @@ This variant implements :
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels (where k *closed* Sort) from 0 or 1 level from 0.
Can only lift k levels from 0 or 1 level from universe i.
;)
......
......@@ -9,7 +9,7 @@ This variant implements :
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels (where k *closed* Sort) from 0 or 1 level from 0.
Can only lift k levels from 0 or 1 level from universe i.
;)
......
#NAME cc.
(; Natural numbers ;)
N : Type.
......@@ -9,7 +7,8 @@ s : N -> N.
def max : N -> N -> N.
[i ] max 0 i --> i
[i ] max i 0 --> i
[i,j] max (s i) (s j) --> s (max i j).
[i,j] max (s i) (s j) --> s (max i j)
[i ] max i i --> i.
B : Type.
......@@ -27,7 +26,8 @@ def le : N -> N -> B.
[i,j] le (s i) (s j) --> le i j
[i] le i i --> true
[i] le (s i) i --> false
[i] le i (s i) --> true.
[i] le i (s i) --> true
[i,j,k] le (max i j) k --> and (le i k) (le j k).
[i,j,k] and (and (le i j) (le j k)) (le i k) --> and (le i j) (le j k)
[i,j,k,c] and (and (and (le i j) (le j k)) (le i k)) c --> and (and (le i j) (le j k)) c.
......@@ -109,6 +109,8 @@ constrain : d : Cstr -> c : Cstr -> i : N -> a : U c i -> U (and d c) i.
(x => constrain (le j k) d j (b x))
).
def u' : c : Cstr -> i : N -> U c (s i) := c => i => constrain c true (s i) (u i).
def u'' : c : Cstr -> i : N -> j : N -> U (and c (le (s i) j)) j :=
......
#NAME idic.
def Cstr := cc.Cstr.
def s := cc.s.
def Sort := cc.N.
......@@ -63,7 +61,7 @@ def g2 : Cstr.
def id :
A : cc.U global Top_1 ->
cc.T global Top_1 A ->
cc.T global Top_1 A := c => A => x => x.
cc.T global Top_1 A := A => a => a.
......@@ -74,39 +72,57 @@ fun (A : Type@{Top.2}) (a : A) => a
(* Top.2 |= *)
;)
def pid :
c : Cstr ->
Top_2 : Sort ->
A : cc.U (and c global) Top_2 ->
cc.T c Top_2 A ->
cc.T c Top_2 A := c => Top_2 => A => x => x.
A : cc.U global Top_2 ->
cc.T global Top_2 A ->
cc.T global Top_2 A
:= Top_2 => A => x => x.
(;
pid_id = pid@{Top.3} (@id) : forall A : Type@{Top.1}, A -> A
(* Top.3 |= Top.1 < Top.3 *)
;)
def Top_3 : Sort.
def g3 : Cstr.
[] g2 -->
(and (sle Set Top_3)
(and (sle Top_1 Top_3)
g3)).
#INFER
(cc.prod
cc.true
(s Top_1)
cc.true
Top_1
(cc.u Top_1)
(A => cc.prod
cc.true
Top_1
cc.true
Top_1
A
(x => A))).
def pid_id :
c : Cstr ->
A : cc.U c Top_1 ->
cc.T c Top_1 A ->
cc.T (and (sle Top_1 Top_3) c) Top_1 A
A : cc.U global Top_1 ->
cc.T global Top_1 A ->
cc.T global Top_1 A
:=
c : Cstr =>
pid (and (sle Top_1 Top_3) c) Top_3
pid Top_3
(cc.lift global
(cc.prod
(and (sle Top_1 Top_3) c)
Top_3
(and (sle Top_1 Top_3) c)
Top_3
(cc.u'' c Top_1 Top_3)
cc.true
(s Top_1)
cc.true
Top_1
(cc.u Top_1)
(A => cc.prod
c
cc.true
Top_1
c
cc.true
Top_1
A
(x => A)))
......
A : Type.
e : A.
def slash : A -> A -> A.
def backslash : A -> A -> A.
def dot : A -> A -> A.
[x] backslash x x --> e.
[x] slash x x --> e.
[x] dot e x --> x.
[x] dot x e --> x.
[x] backslash e x --> x.
[x] slash x e --> x.
[x,y] dot x (backslash x y) --> y.
[x,y] dot (slash y x) x --> y.
[x,y] backslash x (dot x y) --> y.
[x,y] backslash (dot y x) x --> y.
[x,y] slash x (backslash y x) --> y.
[x,y] backslash (slash x y) x --> y.
fun : Type.
plus : fun -> fun -> fun.
mult : fun -> fun -> fun.
minus : fun -> fun -> fun.
id : fun.
0 : fun.
1 : fun.
opp : fun -> fun.
div : fun -> fun -> fun.
ln : fun -> fun.
power : fun -> fun -> fun.
def D : fun -> fun.
[] D id --> 1.
[] D 0 --> 0.
[] D 1 --> 1.
[x,y] D (plus x y) --> plus (D x) (D y).
[x,y] D (mult x y) --> plus (mult y (D x)) (mult x (D y)).
[x,y] D (minus x y) --> minus (D x) (D y).
[x] D (opp x) --> opp (D x).
[x,y] D (div x y) --> minus (div (D x) y) (mult x (div (D y) (mult y y))).
[x] D (ln x) --> div (D x) x.
[x,y] D (power x y) --> plus (mult y (mult (power x (minus y 1)) (D x))) (mult (power x y) (mult (ln x) (D y))).
Group : Type.
1 : Group.
def dot : Group -> Group -> Group.
def inv : Group -> Group.
[x] dot 1 x --> x.
[x] dot x 1 --> x.
[x] dot (inv x) x --> 1.
[x] dot x (inv x) --> 1.
[] inv 1 --> 1.
[x] inv (inv x) --> 1.
[x,y] dot (inv x) (dot x y) --> y.
[x,y] dot x (dot (inv x) y) --> y.
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (f x) --> g (f x).
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (f x) --> g (f x).
[x] g (g x) --> f x.
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (f x) --> f (g (f x)).
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (g x) --> g (g (f x)).
[x] f (g x) --> g (g (g x)).
Dutch : Type.
def w : Dutch -> Dutch.
def r : Dutch -> Dutch.
def b : Dutch -> Dutch.
[x] w (r x) --> r (w x).
[x] b (r x) --> r (b x).
[x] b (w x) --> w (b x).
fun : Type.
plus : fun -> fun -> fun.
mult : fun -> fun -> fun.
minus : fun -> fun -> fun.
id : fun.
0 : fun.
1 : fun.
def D : fun -> fun.
[] D id --> 1.
[] D 0 --> 0.
[] D 1 --> 1.
[x,y] D (plus x y) --> plus (D x) (D y).
[x,y] D (mult x y) --> plus (mult y (D x)) (mult x (D y)).
[x,y] D (minus x y) --> minus (D x) (D y).
A : Type.
def dot : A -> A -> A.
[x,y,z] dot (dot x y) z --> dot x (dot y z).
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -7,3 +5,4 @@ S : Nat -> Nat.
def f : Nat -> Nat -> Nat.
[x,y] f (S x) y --> f x (S x).
[x,y] f x (S y) --> f y x.
#NAME Goodstein.
type : Type.
eps : type -> Type.
......@@ -111,5 +109,6 @@ def Goodstein_bis : Nat -> Nat -> Nat -> Nat.
[seed,remaining,base] Goodstein_bis seed (S remaining) base -->
Goodstein_bis (pred (raise base seed)) remaining (S base).
#SNF GoodsteinAll 3.
#SNF Goodstein 4 2.
\ No newline at end of file
#EVAL GoodsteinAll 3.
#EVAL Goodstein 4 2.
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -12,3 +10,4 @@ def minus : Nat -> Nat -> Nat.
def div : Nat -> Nat -> Nat.
[y] div 0 (S y) --> 0.
[x,y] div (S x) (S y) --> S (div (minus x y) (S y)).
(; 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 Cbv : (Nat -> Nat) -> Nat -> Nat.
[f,x] Cbv f (S x) --> f (S x).
def McCarthy : Nat -> Nat.
def MC_aux : Nat -> Bool -> Nat.
[x] McCarthy x --> Cbv (y => MC_aux y (leq y 100)) x.
[x] MC_aux x True --> McCarthy (McCarthy (plus x 11)).
[x] MC_aux x False --> moins x 10.
def McCarthy_opti : Nat -> Nat.
[x] McCarthy_opti (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) --> (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
[x] McCarthy_opti x --> McCarthy_opti (McCarthy_opti (plus x 11)).
#EVAL McCarthy 1.
#CHECK (McCarthy 1) == 91.
#NAME MillerPatternWithLambda.
A : Type.
f : A -> A -> A.
def g : (A -> A) -> A.
......@@ -16,5 +14,5 @@ a : A.
-->
a.
#CONV g (x => g (y => f x y)), a.
#CONV h (x => g (y => f x y)), a.
#CHECK g (x => g (y => f x y)) == a.
#CHECK h (x => g (y => f x y)) == a.
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -28,6 +26,6 @@ def eq : Nat -> Nat -> Nat.
def e := x : Nat => y : Nat => (eq x y).
#WHNF e.
#HNF e.
#SNF e.
\ No newline at end of file
#EVAL[WHNF] e.
#EVAL[HNF] e.
#EVAL[SNF] e.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[y] plus 0 y --> y.
[x,y] plus (S x) y --> S (plus x y).
def mult : Nat -> Nat -> Nat.
[] mult 0 _ --> 0.
[x,y] mult (S x) y --> plus (mult x y) y.
def f : Nat -> Nat -> Nat.
[x] f x x --> x.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 5 := S (S 3).
#EVAL[WHNF,1] f (plus 3 2) (mult 1 5).
A : Type.
def g : A -> A.
def f : A -> A -> A.
def a : A.
def b : A.
[] g a --> f a b.
[] a --> b.
[x] f x x --> g x.
#EVAL[WHNF] (f a b).
(; retourne g a ;)
#EVAL[SNF] (f a b).
(; retourne g b ;)
#EVAL[WHNF] a.
(; retourne b ;)
#NAME Abstraction.
A : Type.
f: A -> A -> A.
def g: A -> (A -> A).
[x] g x --> (y : A => f y x).
#NAME AndPoly.
Bool : Type.
Nat : Type.
......@@ -46,4 +44,5 @@ def andb : n : Nat -> Bool_ n.
(; ;)
def g : n: Nat -> Bool_ n -> Bool.
[X] g (S (S (S 0))) X --> X True False True.
\ No newline at end of file
[X] g (S (S (S 0))) X --> X True False True.
#NAME append.
A : Type.
Nat: Type.
Z : Nat.
......@@ -17,3 +15,4 @@ def append: n : Nat -> Listn n -> m : Nat -> Listn m -> Listn (plus n m).
[l2] append _ nil _ l2 --> l2
[n,l1,m,l2,a]
append _ (cons n a l1) m l2 --> cons (plus n m) a (append n l1 m l2).
#NAME Associativity.
nat : Type.
0 : nat.
S : nat -> nat.
......@@ -21,4 +19,5 @@ def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
(; The linear version ;)
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat _ (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
(; ;)
\ No newline at end of file
(; ;)
#NAME BadlyTypedLhs.
N : Type.
0 : N.
......@@ -23,5 +21,6 @@ def eB : Bb -> Type.
(;
def phi : eB a -> Bb.
#CHECK a,eB a.
;)
\ No newline at end of file
#CHECK a : eB a.
;)
#NAME BTR.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -28,4 +26,5 @@ Tt : n : Nat -> Vect n -> Type.
(; Another one
b : Tt (S (S 0)) (concat (S (S (S (S (S (S 0)))))) (Cons e 0 Nil) (S 0) (Cons 0 Nil)).
;)
\ No newline at end of file
;)
#NAME bool.
Bool : Type.
def boucle : Bool -> Bool.
[x] boucle x --> boucle x.
#NAME cic.
Nat : Type.
z : Nat.
......
#NAME DeBruijn.
N : Type.
0 : N.
S : N -> N.
......@@ -37,19 +35,20 @@ def subst : N -> DB -> DB -> DB.
def delta := Lam (App (Var 0) (Var 0)).
#NSTEPS #2 beta (App delta delta).
#NSTEPS #19 beta (App delta delta).
#NSTEPS #36 beta (App delta delta).
#EVAL[2] beta (App delta delta).
#EVAL[19] beta (App delta delta).
#EVAL[36] beta (App delta delta).
def id := Lam (Var 0).
#SNF beta (App id id).
#SNF beta (App id delta).
#SNF beta (App delta id).
#EVAL[SNF] beta (App id id).
#EVAL[SNF] beta (App id delta).
#EVAL[SNF] beta (App delta id).
def left := Lam (Lam (Var (S 0))).
def right := Lam (Lam (Var 0)).
#SNF beta (App left id).
#SNF beta (App (App left id) (App delta delta)).
#SNF beta (Lam (App (Lam (Var (S 0))) id)).
\ No newline at end of file
#EVAL[SNF] beta (App left id).
#EVAL[SNF] beta (App (App left id) (App delta delta)).
#EVAL[SNF] beta (Lam (App (Lam (Var (S 0))) id)).
#NAME doubleCommut.
Nat : Type.
0 : Nat.
......@@ -10,4 +8,5 @@ def plus : Nat -> Nat -> Nat.
[m,n] plus (S m) n --> S (plus m n).
[x,y,z] plus x (plus y z) --> plus (plus x y) z.
[x,y,z] plus (plus x y) z --> plus x (plus y z).
\ No newline at end of file
[x,y,z] plus (plus x y) z --> plus x (plus y z).
#NAME Double.
Nat : Type.
0 : Nat.
......@@ -15,5 +13,6 @@ def double_ : Nat -> Nat := x => plus x x.
def f : (Nat -> Nat) -> Nat.
[] f (x=> plus x x) --> 0.
#SNF f double.
#SNF f double_.
\ No newline at end of file
#EVAL f double.
#EVAL f double_.
#NAME DownToZero.
Nat : Type.
0 : Nat.
......@@ -10,4 +8,5 @@ def down : Nat -> Nat.
[n] down (S n) --> down n.
def w : Nat.
[] w --> S w.
\ No newline at end of file
[] w --> S w.
#NAME ExamplesBJO.
type : Type.
arrow : type -> type -> type.
def eval : type -> Type.
......@@ -210,4 +208,5 @@ def intrecBis : A : type -> eval A -> (Int -> eval A -> eval A) -> (Int -> eval
[A, x, y, z, n] intrecBis A x y z (s_int n) --> y n (intrecBis A x y z n).
[A, x, y, z, n] intrecBis A x y z (p_int n) --> z n (intrecBis A x y z n).
def plus_int_rec : Int -> Int -> Int := x => y => intrec int x (x => y => s_int y) (x => y => p_int y) y.
\ No newline at end of file
def plus_int_rec : Int -> Int -> Int := x => y => intrec int x (x => y => s_int y) (x => y => p_int y) y.
#NAME ExamplesBJR.
(; The first nonterminaing example ;)
A : Type.
......@@ -14,4 +12,5 @@ def F : O -> O.
def b : O -> O -&g