Either prove that the following function is χ-computable, or that it is not χ-computable:
is-constant ∈ { p ∈ Exp | p is closed } → Bool
is-constant p = if ∃ v ∈ Exp. ∀ n ∈ ℕ. p ⌜n⌝ ⇓ v then true else false
(Exp is the abstract syntax of χ.)
Either prove that the following function is χ-computable, or that it is not χ-computable:
is-constant ∈ { (f, e) | f ∈ Bool → Bool, e ∈ CExp, e implements f } → Bool
is-constant (f, _) = if ∃ y ∈ Bool. ∀ x ∈ Bool. f x = y then true else false
A member (f, e) of the set { (f, e) | f ∈ Bool → Bool, e ∈ CExp, e implements f } is represented by the representation of e: ⌜(f, e)⌝ = ⌜e⌝.
Either prove that the following function is χ-computable, or that it is not χ-computable:
is-constant ∈ { (f, e) | f ∈ ℕ → Bool, e ∈ CExp, e implements f } → Bool
is-constant (f, _) = if ∃ b ∈ Bool. ∀ n ∈ ℕ. f n = b then true else false
[BN] Write a χ program isNat that, when applied to an argument m, terminates with the value True() if m ⇓ ⌜n⌝ for some n ∈ ℕ, and otherwise does not terminate with a value.
[BN] It seems to be hard to write a χ program isNat that, when applied to an argument m, terminates with the value True() if m ⇓ ⌜n⌝ for some n ∈ ℕ, and terminates with the value False() if m ⇓ v for some v that is not equal to ⌜n⌝ for any n ∈ ℕ.
Suggest a variant of χ for which this program can be implemented. Specify how the abstract syntax and the operational semantics should be modified, and give the implementation of isNat.
[BN] The language χ-PRF is obtained from χ by removing rec, case and const and instead adding natural number constructors (zero ∈ Exp and, for any e ∈ Exp, suc e ∈ Exp) and primitive recursion: if e₁, e₂, e₃ ∈ Exp, then primrec e₁ e₂ e₃ ∈ Exp.
Give a formal operational semantics for χ-PRF.
[BN] Implement Ackermann’s function in χ-PRF.
(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.)