We consider the system monad.

  Alphabet:

    bind : [] --> Ta -> (a -> Ta) -> Ta 
    return : [] --> a -> Ta 

  Rules:

    bind (return x) (/\y.f y) => f x 
    bind x (/\y.return y) => x 
    bind (bind x (/\y.f y)) (/\z.g z) => bind x (/\u.bind (f u) (/\v.g v)) 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    bind : [Ta * a -> Ta] --> Ta 
    return : [a] --> Ta 
    ~AP1 : [a -> Ta * a] --> Ta 

  Rules:

    bind(return(X), /\x.~AP1(F, x)) => ~AP1(F, X) 
    bind(X, /\x.return(x)) => X 
    bind(bind(X, /\x.~AP1(F, x)), /\y.~AP1(G, y)) => bind(X, /\z.bind(~AP1(F, z), /\u.~AP1(G, u))) 
    bind(return(X), /\x.return(x)) => return(X) 
    bind(bind(X, /\x.return(x)), /\y.~AP1(F, y)) => bind(X, /\z.bind(return(z), /\u.~AP1(F, u))) 
    bind(bind(X, /\x.~AP1(F, x)), /\y.return(y)) => bind(X, /\z.bind(~AP1(F, z), /\u.return(u))) 
    bind(bind(X, /\x.return(x)), /\y.return(y)) => bind(X, /\z.bind(return(z), /\u.return(u))) 
    ~AP1(F, X) => F X 

Symbol ~AP1 is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  Additionally, we can remove some (now-)redundant rules.  This gives:

  Alphabet:

    bind : [Ta * a -> Ta] --> Ta 
    return : [a] --> Ta 

  Rules:

    bind(return(X), /\x.Y(x)) => Y(X) 
    bind(X, /\x.return(x)) => X 
    bind(bind(X, /\x.Y(x)), /\y.Z(y)) => bind(X, /\z.bind(Y(z), /\u.Z(u))) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  bind(return(X), /\x.Y(x)) >? Y(X) 
  bind(X, /\x.return(x)) >? X 
  bind(bind(X, /\x.Y(x)), /\y.Z(y)) >? bind(X, /\z.bind(Y(z), /\u.Z(u))) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  bind = \y0G1.3 + 3y0 + G1(y0) + 2y0G1(y0) 
  return = \y0.3 + y0 

Using this interpretation, the requirements translate to:

  [[bind(return(_x0), /\x._x1(x))]] = 12 + 3x0 + 2x0F1(3 + x0) + 7F1(3 + x0) > F1(x0) = [[_x1(_x0)]] 
  [[bind(_x0, /\x.return(x))]] = 6 + 2x0x0 + 10x0 > x0 = [[_x0]] 
  [[bind(bind(_x0, /\x._x1(x)), /\y._x2(y))]] = 12 + 9x0 + 2F1(x0)F2(3 + 3x0 + F1(x0) + 2x0F1(x0)) + 3F1(x0) + 4x0F1(x0)F2(3 + 3x0 + F1(x0) + 2x0F1(x0)) + 6x0F1(x0) + 6x0F2(3 + 3x0 + F1(x0) + 2x0F1(x0)) + 7F2(3 + 3x0 + F1(x0) + 2x0F1(x0)) > 6 + 9x0 + F2(F1(x0)) + 2x0F2(F1(x0)) + 2F1(x0)F2(F1(x0)) + 3F1(x0) + 4x0F1(x0)F2(F1(x0)) + 6x0F1(x0) = [[bind(_x0, /\x.bind(_x1(x), /\y._x2(y)))]] 

We can thus remove the following rules:

  bind(return(X), /\x.Y(x)) => Y(X) 
  bind(X, /\x.return(x)) => X 
  bind(bind(X, /\x.Y(x)), /\y.Z(y)) => bind(X, /\z.bind(Y(z), /\u.Z(u))) 

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ Citations +++

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.