やったー、Coqでのたらい回し関数の停止性証明できたよー - kururu_goedel’s diaryCall-by-name版なので簡単ですけど。ものすごく下手なソースだと思いますが、一応晒しておきます。 Require Import ZArith. Require Import List. Open Scope Z_scope. Fixpoint ntarai3 (n : nat) (a b c : option Z) := match a with | None => None | Some av => match b with | None => None | Some bv => if Z_le_dec av bv then b else match n with | 0%nat => None | S np => match c with | None => None | Some cv => (ntarai3 np (ntarai3 np (Some (av-1)) b c)
