See
https://github.com/luciangreen/mi
https://github.com/luciangreen/mi2
https://github.com/luciangreen/mi3
Below are concrete example predicates you can feed to each mi*.pl, and the typical outputs you would expect based on how each system works.
I’ll use the following test predicates because they represent the major classes of recursion:
1. numeric recursion (sum)
2. multiplicative recursion (factorial)
3. list recursion (length)
4. list recursion with head contribution (sumlist)
5. accumulator wrapper (reverse)
6. nested recursion (Fibonacci)
⸻
- mi.pl (trace + polynomial fitting + pattern guessing)
Example 1 — Sum 1..N
Input
sum_to(0,0).
sum_to(N,S) :-
N>0,
N1 is N-1,
sum_to(N1,S1),
S is S1+N.
Call
?- analyze_predicates([sum_to(0,0),
(sum_to(N,S):-N>0,N1 is N-1,sum_to(N1,S1),S is S1+N)], R).
Typical Output
[
tagged(pattern(expr(nested,sum)), reusable(pattern_1234,3)),
tagged(pattern(expr(nested,sum)), reusable(pattern_5678,2))
]
Or after flattening / solving:
Closed form: n*(n+1)/2
This occurs because mi.pl traces values like:
N: 0 1 2 3 4
S: 0 1 3 6 10
and polynomial-fits them.
⸻
Example 2 — Factorial
Input
fact(0,1).
fact(N,R) :-
N>0,
N1 is N-1,
fact(N1,R1),
R is N*R1.
Output (approximate)
Closed form: factorial(N)
This usually comes from a placeholder recognizer:
recognize_factorial_pattern(...)
⸻
Example 3 — Fibonacci
Input
fib(0,0).
fib(1,1).
fib(N,F) :-
N>1,
fib(N-1,F1),
fib(N-2,F2),
F is F1+F2.
Typical output
Detected: nested recursion
Formula: unsupported / guessed
Or sometimes:
formula = ((phi^n - psi^n)/sqrt(5))
but this is pattern recognition, not derived mathematically.
⸻
- mi2.pl (real recurrence extraction)
This system analyses clause structure.
⸻
Example 1 — Sum 1..N
Input
sum_to(0,0).
sum_to(N,S) :-
N>0,
N1 is N-1,
sum_to(N1,S1),
S is S1+N.
Call
?- analyze_predicate(Clauses, sum_to, 2, Analysis).
Output
analysis{
predicate:sum_to/2,
status:supported,
recurrence:recurrence{
domain:integer,
input_var:n,
base_cases:[base_case(0,0)],
step:step{
transform:dec(1),
combiner:add(current_n)
}
},
closed_form:closed_form{
kind:sum_1_to_n,
formula:n*(n+1)//2
}
}
⸻
Example 2 — Factorial
Input
fact(0,1).
fact(N,F) :-
N>0,
N1 is N-1,
fact(N1,F1),
F is N*F1.
Output
analysis{
predicate:fact/2,
status:supported,
recurrence:recurrence{
domain:integer,
base_cases:[base_case(0,1)],
step:step{
transform:dec(1),
combiner:multiply(current_n)
}
},
closed_form:closed_form{
kind:factorial,
formula:factorial(n)
}
}
⸻
Example 3 — List Length
Input
len([],0).
len([_|T],N) :-
len(T,N1),
N is N1+1.
Output
analysis{
predicate:len/2,
status:supported,
recurrence:recurrence{
domain:list,
base_cases:[base_case([],0)],
step:step{
transform:tail,
combiner:add(constant(1))
}
},
closed_form:closed_form{
kind:list_length,
formula:length_of(xs)
}
}
⸻
Example 4 — Fibonacci
Input
fib(0,0).
fib(1,1).
fib(N,F) :-
N>1,
fib(N-1,F1),
fib(N-2,F2),
F is F1+F2.
Output
analysis{
predicate:fib/2,
status:unsupported,
reason:nested_recursion
}
This is correct behaviour.
⸻
- mi3.pl (pattern recognizer)
This is the system you recently debugged.
⸻
Example 1 — Sum
Input
sum_to(0,0).
sum_to(N,S) :-
N>0,
N1 is N-1,
sum_to(N1,S1),
S is S1+N.
Output
Predicate: sum_to/2
Status: supported
Recurrence:
recurrence{
base_cases:[base_case(0,0)],
domain:integer,
step:step{
transform:dec(1),
combiner:add(current_n)
}
}
Closed form:
closed_form{
formula:n*(n+1)//2,
kind:sum_1_to_n
}
⸻
Example 2 — Factorial
Input
fact(0,1).
fact(N,F) :-
N>0,
N1 is N-1,
fact(N1,F1),
F is N*F1.
Output
Closed form:
factorial(n)
⸻
Example 3 — List length
Input
len([],0).
len([_|T],N) :-
len(T,N1),
N is N1+1.
Output
Closed form:
length_of(xs)
⸻
Example 4 — Sumlist
Input
sumlist([],0).
sumlist([H|T],S) :-
sumlist(T,S1),
S is S1+H.
Output
Closed form:
sum_of(xs)
⸻
Example 5 — Reverse accumulator
Input
rev(L,R) :- rev_acc(L,[],R).
rev_acc([],A,A).
rev_acc([H|T],A,R) :-
rev_acc(T,[H|A],R).
Output
Predicate: rev/2
Status: supported
Recurrence:
accumulator_only
Closed form:
normalizable_tail_recursion
⸻
ChatGPT: If you’d like, I can also show you three predicates that break all three systems (true nested recursion and tree recursion), which reveals the current theoretical boundary of these architectures.
Top comments (0)