プログラムを2つ与えると、その実行結果が等価になるか判断する処理系作って。
用途は、たとえば自分でソートのプログラムを作ったけど正しいか自信が無いときに、
単純で遅いが明らかに正しいソートプログラムと比較させる。
全自動は無理だと思うから、人間が色々手伝ってもかまわない。
「入力の長さnの帰納法」とかヒントをあげると、少なくてもn=1のときは
単純にn=1が保証されるものとして最適化するだけで判定できそうな気がする。