# Phil 455: Homework 5

This homework is due by the end of the day on Wed, Feb 28.

Reminder of some of the definitions we already formulated:

``````isUnit =def {
λ ""! false;
λ α ⁀ β if α ≠ "" and β ≠ ""! false;
λ α. true
}

length =def {
λ "". 0;
λ α ⁀ β if isUnit(α). 1 + length(β)
}

startsWith (γ, δ) =def dissect γ {
λ α ⁀ β if α = δ! true;
λ β. false
}``````
1. Define `endsWith (γ, δ)`, which returns `true` iff `δ` is (assigned or bound to) some string which is the suffix of `γ` (what `γ` is assigned or bound to).

2. Define `anyWhere (γ, δ)`, which returns `true` iff `δ` is some string which occurs at the start of `γ`, or in the middle, or at the end. Explain what decision you made about whether to count the empty string or `"dog"` as occurring anywhere inside the string `"dog"`.

3. Here is a defintion of a function that takes a string and a number as argument, and gives a string as a result.

``````take (γ, x) =def dissect γ {
λ β if x = 0! "";
λ "". "";
λ α ⁀ β if isUnit(α). α ⁀ take(β, x - 1)
}``````
1. What is the result of `take("abc", 2)`?
2. What is the result of `take("", 2)`?
3. What is the result of `take("abc", 5)`?
4. What is the result of `take("abc", 0)`?
4. Define a function `drop (γ, x)` which works similarly to `take`, except where `take` would keep the first `x` characters and discard the rest, `drop` discards the first `x` characters and keeps the rest. Explain what decision you made about what results to return for `drop("", 2)` and `drop("abc", 5)`.

5. Consider the following definitions.

``````oneVowel =def {
λ "a"! true;
λ "e"! true;
λ "i"! true;
λ "o"! true;
λ "u"! true;
λ β. false
}

vowels =def {
λ ""! true;
λ α ⁀ β if oneVowel(α)! vowels(β);
λ β. false
}``````
1. What is the result of `oneVowel("ea")`?
2. What is the result of `oneVowel("")`?
3. What is the result of `vowels("ea")`?
4. What is the result of `vowels("eat")`?
6. Consider the following definition:

``````takeWhile1 (γ, Q) =def dissect γ {
λ α ⁀ β if isUnit(α) and Q(α)! α ⁀ takeWhile1 (β, Q);
λ β. ""
}``````

Something new is going on here. The argument `Q` is not a string or a number but instead a predicate, like for example `isUnit` or `oneVowel` or `vowels`. (Since we are binding some variables to predicates, our formalism counts as higher-order.)

1. What is the result of `takeWhile1("dog", oneVowel)`?
2. What is the result of `takeWhile1("eat", oneVowel)`?
3. What is the result of `takeWhile1("eat", isUnit)`?
7. Define a function `dropWhile1 (γ, Q)` which works similarly to `takeWhile1`, except where `takeWhile1` keeps the longest prefix of `γ` whose units each satisfy `Q` and discards the rest, `dropWhile1` discards that prefix and keeps the rest. Explain what decision you made about what results to return for `dropWhile1("", oneVowel)` and `dropWhile1("ea", oneVowel)`.

8. This will be somewhat harder than other problems. Don’t worry if it’s too hard. I want you to try it, but will take its difficulty into account when grading. Consider the definition:

``````takeWhile2 (γ, Q, δ) =def dissect γ {
λ α ⁀ β if α ≠ "" and Q(δ ⁀ α)! takeWhile2 (β, Q, δ ⁀ α);
λ β. δ
}``````
1. What is the result of `takeWhile2("dog", oneVowel, "")`?

2. What is the result of `takeWhile2("eat", oneVowel, "")`?

3. What is the result of `takeWhile2("eat", vowels, "")`?

4. What is the result of `takeWhile2("eat", isUnit, "")`?

5. Will the result of `takeWhile2(γ, Q, "")` always satisfy the predicate `Q`? If so, explain why. If not, when will this fail?

9. For this problem, you don’t need to apply or construct a definition. Instead you need to give an inductive argument. Consider all the strings that have `"t"` as a suffix. Prove that any such string has a length `> 0`.

Hint: The strings we are considering are all of the form `δ ⁀ "t"`. Your base step is when `δ` is `""`. The induction step assumes that the thesis has been established for when `δ` is some string `η`, and has to argue that it would then also hold when `δ` is `α ⁀ η` for some unit string `α`.

10. We say that the reverse of a string `"abc"` is `"cba"`. We can define that notion like this:

``````reverse =def {
λ "". "";
λ α ⁀ β if isUnit(β). β ⁀ reverse(α)
}``````
1. What is `reverse("")`?
2. What is `reverse("t")`?
3. What is `reverse("abba")`?
11. As in Problem 64, here again you need to give an argument, rather than apply or construct a definition. Observe that `reverse("abcde")` is the same as `reverse("de") ⁀ reverse("abc")`, which is `"ed" ⁀ "cba"`. Prove that in general, `reverse(γ ⁀ δ) = reverse(δ) ⁀ reverse(γ)`.

Hint: Just do induction on one of the arguments, let’s say `δ`. Your base step is when `δ` is `""`. The induction step assumes that the thesis has been established for when `δ` is some string `η`, and has to argue that it would then also hold when `δ` is `η ⁀ β` for some unit string `β`.

12. Sometimes we might want to talk about strings that encode structures (for example, sequences) of other strings. Let’s adopt the following conventions. We’ll use the colon (`:`) as a marker between elements of our sequence. Then we’ll encode the empty sequence as `":"`. We’ll encode the sequence which contains the string `"abc"` as `":abc:"`. We’ll encode the sequence which contains the string `"abc"` followed by the string `"def"` as `":abc:def:"`. We’ll encode the sequence which contains the string `"abc"` followed by the empty string as `":abc::"`. In every case, our sequence is a string that starts and ends with a colon. (If it’s the empty sequence, this is the same colon.) And whatever comes between two colons is another element in the sequence. No element of the sequence can itself contain a colon.

We’re not introducing any new formalism. `":abc::"` is still just a string consisting of the unit string `":"` concatenated to `"a"` and then to `"b"` and so on. But we’re interpeting this string as standing for the sequence of two strings, `"abc"` followed by `""`.

We can define functions to work on strings interpreted in this way. Consider the following function:

``````headOf =def {
λ ":" ⁀ α ⁀ β if not anyWhere(α, ":") and startsWith(β, ":") and endsWith(β, ":")!! α;
λ β if startsWith(β, ":") and endsWith(β, ":")! ":";
λ β. undefined
}``````

This could equivalently be written as:

``````headOf =def {
λ ":" ⁀ α ⁀ β if not anyWhere(α, ":") and startsWith(β, ":")! α;
λ β. ":"
} assuming { λ β if startsWith(β, ":") and endsWith(β, ":") }``````
1. What is `headOf(":abc::")`?
2. What is `headOf("::abc:")`?
3. What is `headOf(":")`?
4. What is `headOf` applied to a string that doesn’t encode a sequence according to our conventions, like `""` or `":abc"` or `"abc:"`?
13. Define a function `tailOf`, which works similarly to `headOf`, except where `headOf` keeps the first element of the encoded sequence (if any), and discards the rest, `tailOf` discards the first and keeps the rest. Explain what decision you made about what result to return for `tailOf(":")`.

14. Consider this definition. The argument `Q` is a predicate on strings.

``````anyOf (γ, Q) =def dissect γ {
λ ":"! false;
λ ":" ⁀ α ⁀ β if not anyWhere(α, ":") and startsWith(β, ":") and Q(α)! true;
λ ":" ⁀ α ⁀ β if not anyWhere(α, ":") and startsWith(β, ":"). anyOf(β, Q)
} assuming { λ β if startsWith(β, ":") and endsWith(β, ":") }``````
1. What is `anyOf(":a:b:c:", oneVowel)`?
2. What is `anyOf(":b:", oneVowel)`?
3. What is `anyOf(":", oneVowel)`?