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 ∈ Bool → Bool | f is χ-computable } → Bool
is-constant f = if ∃ y ∈ Bool. ∀ x ∈ Bool. f x = y then true else false
Elements of the set { f ∈ Bool → Bool | f is χ-computable } are represented by the representation of closed χ expressions witnessing the χ-computability of the functions.
Either prove that the following function is χ-computable, or that it is not χ-computable:
is-constant ∈ { f ∈ ℕ → Bool | f is χ-computable } → 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 ∈ ℕ.
[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 and case and instead adding primitive recursion: if e₁, e₂, e₃ ∈ Exp, then primrec e₁ e₂ e₃ ∈ Exp. The idea of primrec is that primrec e₁ e₂ Zero() reduces to e₁, and that primrec e₁ e₂ Succ(n) reduces to e₂ n (primrec e₁ e₂ n).
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.)