Inductive term : Type :=
| var (n : nat) : term
| app (s : term) (t : term) : term
| lam (s : term).
Fixpoint subst (s : term) (k : nat) (u : term) :=
match s with
| var n => if Nat.eqb n k then u else var n
| app s t => app (subst s k u) (subst t k u)
| lam s => lam (subst s (S k) u)
end.
Inductive eval : term -> term -> Prop :=
| eval_abs s : eval (lam s) (lam s)
| eval_app s u t t' v :
eval s (lam u) -> eval t t' -> eval (subst u 0 t') v -> eval (app s t) v.
Definition HaltL (s : term) := exists t, eval s t.
Fixpoint nat_enc (n : nat) :=
match n with
| 0 => lam (lam (var 1))
| S n => lam (lam (app (var 0) (nat_enc n)))
end.
Require Import Vector.
Definition L_computable {k} (R : Vector.t nat k -> nat -> Prop) :=
exists s, forall v : Vector.t nat k, forall m,
R v m <->
eval (Vector.fold_left (fun s n => app s (nat_enc n)) s v) (nat_enc m).