import java.util.function.Function;

/**
 * Demonstration of Fixed Point Theorem for calculating a non-total function.
 */
public class LeastFixedPoint {

  // bottom, represented as infinite loop
  final Function<Integer, Integer> undefined = (a) -> this.undefined.apply(a);
  // bottom, represented as throwing exception
  final Function<Integer, Integer> undefined_ex = new Function<Integer, Integer>() {
    @Override
    public Integer apply(Integer a) {
      throw new RuntimeException("Undefined");
    }
  };


  // FUNC is a function that returns 5 when input is even and has undefined behavior for odd inputs
  // conveniently works out even if passed any bottom for parameter 'f' as f.apply is not evaluated if n == 0
  final Function<Function<Integer, Integer>, Function<Integer, Integer>> FUNC = (f) -> (n) -> n == 0 ? 5 : (n == 1 ? f.apply(n+2) : f.apply(n-2));

  // A fixed point of FUN. Note this is not the least fixed point
  final Function<Integer, Integer> g = (a) -> 5;

  public Function<Integer, Integer> compose(Function<Integer, Integer> bottom, int times) {
    Function<Integer, Integer> t = bottom;

    // expand FUNC 'times' times and it is LUB of the F(F(F..)) chain of size 'times'
    while (times-- > 0) {
      t = FUNC.apply(t);
    }
    return t;
  }

  public static void main(String[] args) {
    LeastFixedPoint fp = new LeastFixedPoint();
    // fp.undefined.apply(new Integer(10)); // in theory infinite loop; in reality stack overflow or throws exception or abnormal exit
    Function<Integer, Integer> bottom = fp.undefined_ex; // i.e., used to apply the case where recursion is not involved=terminal condition.


    int n = 10; // FUNC is defined
    Function<Integer, Integer> lub = fp.compose(bottom, n+1);
    System.out.println(String.format("using lub for a defined input, n = %d, result = %d", n, lub.apply(n)));

    n = 11; // FUNC is undefined, hence throws exception due to choice of bottom above
    lub = fp.compose(bottom, n+1);
    try {
      System.out.println(lub.apply(n));
    } catch (Throwable t) {
      System.out.println(String.format("using lub for an undefined input, n = %d, result = <throws exception>", n));
      System.out.println(t);
    }

    Function<Integer, Integer> ub = fp.g;   // ub is more defined than 'necessary' whereas lub is defined to be just enough to match the semantics of FUN
    n = 10;
    System.out.println(String.format("using ub for a defined input, n = %d, result = %d", n, ub.apply(n)));
    n = 11;
    System.out.println(String.format("using ub for an undefined input, n = %d, result = %d", n, ub.apply(n)));
    // just to show that ub is a fixed point of FUNC
    System.out.println(String.format("using ub to show that it is a fixed point for a defined input, n = %d, result = %d", n, fp.compose(fp.g, 100).apply(n)));
  }

}