Injective: f, g. Surjective: g, h.
Yes. Injection to ℕ: Take the binary representation of the string (padded so that each character has the same “width”), and prepend a one.
No.
No.
rec (λ n. n) (λ m r. λ n. suc (r n)).
2.
rec (proj 0) (comp suc (nil, proj 1)).
comp zero nil [nil, 5, 7] ⇓ 0 and rec zero (proj 1) [nil, 2] ⇓ 0.
min suc.
Suc(Zero()).
λ x. λ y. x, case Suc(Zero()) of { Suc(x) → x } and rec f = λ x. f.
rec y = case λ z. z of { C() → λ z. z; D(x) → x }.
case C() of { C() → D(); C() → C() } ⇓ D() and case Suc(False()) of { Zero() → True(); Suc(n) → n } ⇓ False().
Rec(Suc(Zero()), Var(Suc(Zero()))).
The halting problem would be “computable”.
Yes: λ p. (λ x. True()) (eval p).
See the slides.
We can reason in the following way:
⟦ (λ p. eval ⌜eval ⌞code p⌟⌝) ⌜Zero()⌝ ⟧ =
⟦ (λ p. eval Apply(⌜eval⌝, code p)) ⌜Zero()⌝ ⟧ =
⟦ eval Apply(⌜eval⌝, code ⌜Zero()⌝) ⟧ =
⟦ eval Apply(⌜eval⌝, ⌜⌜Zero()⌝⌝) ⟧ =
⟦ eval ⌜eval ⌜Zero()⌝⌝ ⟧ =
⌜⟦ eval ⌜Zero()⌝ ⟧⌝ =
⌜⌜⟦ Zero() ⟧⌝⌝ =
⌜⌜Zero()⌝⌝Note that for any expression e we have ⟦ code ⌜e⌝ ⟧ = ⌜⌜e⌝⌝, and if e is closed we also have ⟦ eval ⌜e⌝ ⟧ = ⌜⟦ e ⟧⌝.
See the slides.
Is e ∈ CExp syntactically equal to λ n. Suc(n)?
The other problem is not χ-decidable. This can be proved using Rice’s theorem. Define P ∈ CExp → Bool in the following way:
P e = if ∀ n ∈ ℕ. ⟦ e ⌜n⌝ ⟧ = ⌜suc n⌝ then true else false
This function is non-trivial: P (λ n. Suc(n)) = true and P Zero() = false. It also respects pointwise semantic equality: for any e₁, e₂ ∈ CExp we have
(∀ e ∈ CExp. ⟦ e₁ e ⟧ = ⟦ e₂ e ⟧) ⇒
(∀ n ∈ ℕ. ⟦ e₁ ⌜n⌝ ⟧ = ⟦ e₂ ⌜n⌝ ⟧) ⇒
P e₁ = P e₂.
act (0, R) (act (1, R) ([], [])) = ([0, 1], []).
It is deterministic. There are Turing machines for which it is not total.
1010.
Those of even length.
[3, 0, 2, 0].
None.
⌜tm⌝ ++ ⌜⌜tm⌝⌝.
A: No, the left string must end with 01, whereas the right string must end with 00 or 10.
B: Yes, 010 01 = 01 001.
(ℕ → A) → (Tree → Tree → A → A → A) → Tree → A.
If h̲a̲l̲t̲s̲ is applied to ⌜p⌝, then the value of the argument given to p̲o̲i̲n̲t̲w̲i̲s̲e̲-̲e̲q̲u̲a̲l̲ is ⌜(λ n. t̲e̲r̲m̲i̲n̲a̲t̲e̲s̲-̲i̲n̲ Pair(p, n))⌝. However, t̲e̲r̲m̲i̲n̲a̲t̲e̲s̲-̲i̲n̲ should be given the representation of a program: the argument should be ⌜(λ n. t̲e̲r̲m̲i̲n̲a̲t̲e̲s̲-̲i̲n̲ Pair(⌜p⌝, n))⌝. The problem can be fixed by replacing the last occurrence of p with code p.