comp — Mathlib

English

Composition of partial two-argument functions with a computable function preserves partial recursiveness.

Русский

Композиция частично двуарных функций с вычислимой сохраняет частичную рекурсивность.

LaTeX

$$$\forall f:\gamma \to^. \sigma,\forall g:\alpha \to \beta,\forall h:\alpha \to \gamma,\ Partrec_2(f) \rightarrow Computable(g) \rightarrow Computable(h) \rightarrow Partrec_2(\lambda a,b. f(g(a,b), h(a,b))).$$

Lean4

nonrec theorem comp {f : β → γ →. σ} {g : α → β} {h : α → γ} (hf : Partrec₂ f) (hg : Computable g) (hh : Computable h) :
    Partrec fun a => f (g a) (h a) :=
  hf.comp (hg.pair hh)

Похожие утверждения