Confluence Problems (Cops)

759 problems found.
PREV « 1 2 3 4 10 20 26 » NEXT order: desc asc

759.trs

(FUN
  abs : (value -> term) -> value
  emb : value -> term
  app : term -> term -> term
)
(VAR
  x : value
  M : value -> term
  V : value
  N : term
  L : term
)
(RULES
  app (emb (abs (\x. M x))) (emb V) -> M V,
  app (app (emb (abs \x. M x)) N) L -> app (emb (abs \x.app (M x) L)) N,
  app (emb V) (app (emb (abs \x. M x)) N) -> app (emb (abs \x. app (emb V) (M x))) N
)
(COMMENT Carraro and Guerrieri's call-by-value lambda calculus,
 taken from the paper Z for Call-by-Value, by 
 Koji Nakazawa1, Ken-etsu Fujita2, and Yuta Imagawa
 in IWC 2017 programme
)
format:
properties:
solved by:

758.trs

(VAR
  d: data
  X: proc 
  Y: proc 
  Z: proc 
  E: data 
  P: data -> proc 
  Q: data -> proc 
)
(FUN
  xplus : proc -> proc -> proc
  xtimes : proc -> proc -> proc
  delta : proc
  sigma : (data -> proc) -> proc
)
(RULES
  xplus(X,X) -> X,
  xtimes(xplus(X,Y),Z) -> xplus(xtimes(X,Z),xtimes(Y,Z)),
  xtimes(xtimes(X,Y),Z) -> xtimes(X,xtimes(Y,Z)),
  xplus(X,delta) -> X,
  xtimes(delta,X) -> delta,
  sigma((\d.X)) -> X,
  xplus(sigma((\d.(P d))),(P E)) -> sigma((\d.(P d))),
  sigma((\d.xplus((P d),(Q d)))) -> xplus(sigma((\d.(P d))),sigma((\d.(Q d)))),
  xtimes(sigma((\d.(P d))),X) -> sigma((\d.xtimes((P d),X)))
)
(COMMENT a variant from Mixed_HO_10)
format:
properties:
solved by:

757.trs

(VAR
  X: nat 
  Y: nat 
  P: nat -> bool
  n: nat
  z: natvar
)
(FUN
  0 : nat
  s : nat -> nat
  err : nat
  pre : nat -> nat
  id : nat -> nat
  add : nat -> nat -> nat
  eq : nat -> natp
  true : bool
  false : bool
  fn : (natvar -> bool) -> natp
  nul : nat -> bool
  at : natp -> nat -> bool
  v : natvar -> nat
)
(RULES
  nul(0) -> true,
  nul(s(X)) -> false,
  nul(err) -> false,
  pre(0) -> err,
  pre(s(X)) -> X,
  id(X) -> X,
  eq(0) -> fn (\z.nul (v z)),
  eq(s(X)) -> fn (\z.at (eq X) (pre (v z))),
  at(fn (\z.P (v z)),n) -> P n
)
(COMMENT a variant from Mixed_HO_10)
format:
properties:
solved by:

756.trs

(VAR
  x: nat 
  n: var
  y: nat 
  U: nat 
  F: nat -> nat -> nat 
  z1: nat
  z2: nat
)
(FUN
  0 : nat
  s : nat -> nat
  xplus : nat -> nat -> nat
  xtimes : nat -> nat -> nat
  rec : nat -> nat -> (nat -> nat -> nat) -> nat
  v : var -> nat
)
(RULES
  xplus(x,0) -> x,
  xplus(x,s(y)) -> s(xplus(x,y)),
  rec(0,U,\z1 z2.F z1 z2) -> U,
  rec(s(v n),U,\z1 z2.F z1 z2) -> F(v n, rec(x,U,\z1 z2.F z1 z2)),
  xtimes(x,y) -> rec(y,0,(\z1.(\z2.xplus(x,z2))))
)
(COMMENT a variant from Mixed_HO_10)
format:
properties:
solved by:

755.trs

(VAR
  F: N -> N 
  X: N 
  Y: N 
  Z: N 
  x: VN
  v: VN -> N
)
(FUN
  o : N
  s : N -> N
  fun : (VN -> N) -> N -> N -> N
  dom : N -> N -> N -> N
  eval : N -> N -> N
)
(RULES
  eval(fun(\x.F (v x),X,Y),Z) -> F(dom(X,Y,Z)),
  dom(s(X),s(Y),s(Z)) -> s(dom(X,Y,Z)),
  dom(o,s(Y),s(Z)) -> s(dom(o,Y,Z)),
  dom(X,Y,o) -> X,
  dom(o,o,Z) -> o
)
(COMMENT a variant from Mixed_HO_10)
format:
properties:
solved by:

754.trs

(VAR
  x: var
  y: var
  F: var -> real 
  G: var -> real 
  M: real -> real
  N: real
)
(FUN
  0 : real
  1 : real
  sin : real -> real
  cos : real -> real
  ln : real -> real
  der : realfun -> realfun
  fn : (var -> real) -> realfun
  evalv : realfun -> var -> real
  eval : realfun -> real -> real
  v : var -> real
)
(RULES
  (der(fn(\x.v y ))) -> fn(\x.(0)),
  (der(fn(\x.v x ))) -> fn(\x.(1)),
  evalv(fn(\x.F x), y) -> F y,
  (der(fn(\x.(sin(v x))))) -> fn(\x.(cos(v x))),
  eval(fn(\x.M (v x)), N) -> M N
)
format:
properties:
solved by:

753.trs

(FUN
  case : SAB -> (A -> C) -> (B -> C) -> C
  inl : A -> SAB
  inr : B -> SAB
  f: A
  a: A
  b: A
)(VAR
  x: A
  y: B
  X: A
  Y: B
  Z: SAB
  F: A -> C
  G: B -> C
  H: SAB -> C
)(RULES
  case(inl(X), \x.F x , \y.G y ) -> F X ,
  case(inr(Y), \x.F x , \y.G y ) -> G Y,
  case(Z,\x.H (inl x), \y.H (inr y)) -> H Z,
  f -> a,
  f -> b
)
(COMMENT a variant from van de Pol, Termination proofs for higher-order rewrite systems, HOA'93, LNCS 816)
format:
properties:
solved by:

752.trs

(FUN
  app : arrAB -> A -> B
  lam : (vA -> B) -> arrAB
  case : SAB -> (A -> C) -> (B -> C) -> C
  inl : A -> SAB
  inr : B -> SAB
  piA : PAB -> A
  piB : PAB -> B
  pair : A -> B -> PAB
  var : vA -> A
)(VAR
  M: A -> B
  N: A
  L: arrAB
  x: vA
  y: B
  X: A
  Y: B
  Z: SAB
  F: A -> C
  G: B -> C
  H: SAB -> C
  M1 : A
  N1 : B
  M2 : PAB
  x0: A
)(RULES
  app(lam(\x.M (var x)), N) -> M N,
  lam(\x.app(L, (var x))) -> L,
  piA(pair(M1,N1)) -> M1,
  piB(pair(M1,N1)) -> N1,
  case(inl(X), \x0.F x0 , \y.G y ) -> F X ,
  case(inr(Y), \x0.F x0 , \y.G y ) -> G Y 
)
(COMMENT A subsystem of Roberto Di Cosmo, Delia Kesner: A Confluent Reduction for the Extensional Typed lambda-Calculus with Pairs, Sums, Recursion and terminal Object, ICALP 1993: 645-656)
format:
properties:
solved by:

751.trs

(FUN
  abs : (a -> b) -> ab
  app : ab -> a -> b
  absBG : (BGa -> BGb) -> BGaBGb
  appBG : BGaBGb -> BGa -> BGb
  banga : a -> BGa
  let : BGa -> (a -> BGb) -> BGb
)
(VAR
  M: a -> b
  N: a
  S: ab
  x: a
  M1: BGa -> BGb
  N1: BGa
  S1: BGaBGb
  x1: BGa
  L: BGa
  P: BGaBGb
  C: BGa -> BGb
  Q: a -> BGb
  R: a
)
(RULES
  app(abs(\x.M x), N) -> M N,
  abs(\x.app(S, x)) -> S,
  appBG(absBG(\x1.M1 x1), N1) -> M1 N1,
  absBG(\x1.appBG(S1, x1)) -> S1,
  let(L, \x. appBG(P, (banga x))) -> appBG(P, L),
  let(banga(R), \x.Q x) -> Q R,
  let(L, \x.C (banga x)) -> C L
)
(COMMENT A Yet Simpler Rewriting System for 
 the Linear Lambda Calculus [Ohta-Hasegawa RTA'06] Remark 1)
format:
properties:
solved by:

750.trs

(FUN
  abs : (a -> b) -> ab
  app : ab -> a -> b
  absBG : (BGa -> BGb) -> BGaBGb
  appBG : BGaBGb -> BGa -> BGb
  banga : a -> BGa
  let : BGa -> (a -> BGb) -> BGb
)(VAR
  M: a -> b
  N: a
  S: ab
  x: a
  M1: BGa -> BGb
  N1: BGa
  S1: BGaBGb
  x1: BGa
  L: BGa
  P: BGaBGb
  C: BGa -> BGb
  Q: a -> BGb
  R: a
)(RULES
  app(abs(\x.M x), N) -> M N,
  abs(\x.app(S, x)) -> S,
  appBG(absBG(\x1.M1 x1), N1) -> M1 N1,
  absBG(\x1.appBG(S1, x1)) -> S1,
  let(banga(R), \x.Q x) -> Q R,
  let(L, \x.C (banga x)) -> C L
)
(COMMENT A Rewriting System for 
 the Linear Lambda Calculus [Ohta-Hasegawa RTA'06] Sec.3.2, without commuting conversions)
format:
properties:
solved by:

749.trs

(FUN
  abs : (a -> b) -> ab
  app : ab -> a -> b
  absBG : (BGa -> BGb) -> BGaBGb
  appBGaBGb : BGaBGb -> BGa -> BGb
  appBGbBGc : BGbBGc -> BGb -> BGc
  banga : a -> BGa
  let : BGa -> (a -> BGb) -> BGb
  letbc : BGb -> (b -> BGc) -> BGc
  letBGaBGb : BGa -> (a -> BGaBGb) -> BGaBGb
  letac : BGa -> (a -> BGc) -> BGc
)
(VAR
  M: a -> b
  N: a
  S: ab
  x: a
  M1: BGa -> BGb
  N1: BGa
  S1: BGaBGb
  S2: BGbBGc
  x1: BGa
  L: BGa
  C: BGa -> BGb
  Q: a -> BGb
  P: BGa -> a -> BGb
  K: b -> BGc
  y: b
  bc : BGc
)
(RULES
  app(abs(\x.M x), N) -> M N,
  abs(\x.app(S, x)) -> S,
  appBGaBGb(absBG(\x1.M1 x1), N1) -> M1 N1,
  absBG(\x1.appBGaBGb(S1, x1)) -> S1,
  let(banga(N), \x.Q x) -> Q N,
  let(L, \x.C (banga x)) -> C L,
  letbc(let(L,\x.Q x), \y.K y) -> letac(L, \x.letbc(Q x,\y.K y)),
  appBGbBGc(S2,let(L,\x.Q x)) -> letac(L, \x.appBGbBGc(S2, Q x))
)
(COMMENT A Rewriting System for 
 the Linear Lambda Calculus [Ohta-Hasegawa RTA'06] Sec.3.2, with (com2)(com4))
format:
properties:
solved by:

748.trs

(FUN
  app : arrab -> a -> b
  lam : (Va -> b) -> arrab
  var : Va -> a
  pia : prodab -> a
  pib : prodab -> b
  pair : a -> b -> prodab
)
(VAR
  x : Va
  M : a -> b
  N : a
  L : arrab
  M1 : a
  N1 : b
  M2 : prodab
)
(RULES
  app(lam(\x.M (var x)), N) -> M N,
  lam(\x.app(L, (var x))) -> L,
  pia(pair(M1,N1)) -> M1,
  pib(pair(M1,N1)) -> N1
)
(COMMENT The simply-typed lambda calculus with binary products)
format:
properties:
solved by:

747.trs

(FUN
  app : arrab -> a -> b
  lam : (Va -> b) -> arrab
  var : Va -> a
)
(VAR
  x : Va
  M : a -> b
  N : a
  L : arrab
)
(RULES
  app(lam(\x.M (var x)), N) -> M N,
  lam(\x.app(L, (var x))) -> L
)
(COMMENT The simply-typed lambda calculus beta-eta)
format:
properties:
solved by:

746.trs

(FUN
  app : arrab -> a -> b
  lam : (Va -> b) -> arrab
  var : Va -> a
)
(VAR
  x : Va
  M : a -> b
  N : a
)
(RULES
  app(lam(\x.M (var x)), N) -> M N
)
(COMMENT The simply-typed lambda calculus in the style of second-order algebraic theory [Fiore, Plotkin, Turi LICS'99][Fiore PPDP'02])
format:
properties:
solved by:

745.trs

(FUN
  c : v -> a
  d : v -> a
  f : (v -> b) -> b
  0 : b
)
(VAR
  x : v
  M : a -> b
)
(RULES
  f(\x.M (c(x))) -> 0,
  f(\x.M (d(x))) -> 0
)
format:
properties:
solved by:

744.trs

(FUN
  c : v -> a
  d : v -> a
  f : (v -> b) -> b
  0 : b
  1 : b
)
(VAR
  x : v
  M : a -> b
)
(RULES
  f(\x.M (c(x))) -> 1,
  f(\x.M (d(x))) -> 0
)
format:
properties:
solved by:

743.trs

(FUN
  c : v -> a
  g : b -> b
  0 : b
  1 : b
)
(VAR
  x : v
  M : a -> b
)
(RULES
  g(M(c(x))) -> 1,
  g(0) -> 0
)
format:
properties:
solved by:

742.trs

(VAR
  F: o -> o 
)
(FUN
  f : o -> o
  a : o
)
(RULES
  f(F(a)) -> a
)
format:
properties:
solved by:

741.trs

(VAR x)
(RULES
  if(true, a, x) -> a
  if(true, b, x) -> b
  if(true, g(a), x) -> g(a)
  if(true, g(b), x) -> g(b)
  if(false, x, a) -> a
  if(false, x, b) -> b
  if(false, x, g(a)) -> g(a)
  if(false, x, g(b)) -> g(b)
  g(a) -> g(g(a))
  g(b) -> a
  f(a, b) -> b
  f(g(g(a)), x) -> b
)
(COMMENT handcraftet "UNC & ~NFP")
format:
properties:
solved by:

740.trs

(VAR x)
(RULES
  f(a, f(x, a)) -> f(a, f(f(a, a), a))
)
(COMMENT UN & ~UNC)
format:
properties:
solved by:

739.trs

(VAR x)
(RULES
  a -> a
  g(g(a)) -> b
  g(g(x)) -> g(g(g(b)))
)
(COMMENT UN & ~UNC)
format:
properties:
solved by:

738.trs

(VAR x)
(RULES
  a -> a
  f(b, a) -> f(a, b)
  f(x, a) -> b
)
(COMMENT UN & ~NFP)
format:
properties:
solved by:

737.trs

(VAR x)
(RULES
  f(a, f(a, x)) -> b
)
(COMMENT UNC & ~NFP)
format:
properties:
solved by:

736.trs

(VAR x)
(RULES
  a -> a
  f(f(x, a), a) -> b
)
(COMMENT UNC & ~NFP & ~SN)
format:
properties:
solved by:

735.trs

(RULES
  a -> a
  a -> b
  f(a, a) -> f(b, f(f(a, b), a))
)
(COMMENT NFP & ~CR)
format:
properties:
solved by:

734.trs

(VAR x)
(RULES
  f(a, f(a, x)) -> f(f(a, a), a)
)
(COMMENT NFP & ~CR)
format:
properties:
solved by:

733.trs

(VAR x0)
(RULES
  a -> a
  a -> b
  a -> f(a, a)
  f(b, b) -> f(a, b)
  f(x0, a) -> f(b, b)
)
(COMMENT -f "a:0 b:0 f:2" -r 5 "UN & ~UNC & GUNC")
format:
properties:
solved by:

732.trs

(VAR x0)
(RULES
  a -> a
  a -> b
  a -> f(a, a)
  f(b, b) -> f(a, a)
  f(x0, a) -> f(a, b)
)
(COMMENT -f "a:0 b:0 f:2" -r 5 "UN & ~UNC & ~SN")
format:
properties:
solved by:

731.trs

(VAR x)
(RULES
  a -> a
  a -> b
  f(b, b) -> f(a, b)
  f(x, a) -> f(a, b)
)
(COMMENT -f "a:0 b:0 f:2" -r 4 "UN & ~UNC & ~SN")
format:
properties:
solved by:

730.trs

(FUN
  get: S -> V
  put: S -> V -> S
)
(VAR
  X: S
  Y: V
)
(RULES
  put(X, get(X)) -> X,
  get(put(X, Y)) -> Y,
  put(put(X, Y), Y) -> put(X, Y)
)
(COMMENT Well-behaved lens laws, A clear picture of lens laws, Sebastian Fischer, Zhenjiang Hu, and Hugo Pacheco, MPC'15)
format:
properties:
solved by:
PREV « 1 2 3 4 10 20 26 » NEXT order: desc asc