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
}

Define endsWith (γ, δ), which returns true iff δ is (assigned or bound to) some string which is the suffix of γ (what γ is assigned or bound to).
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".
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)?
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).

Consider the following definitions.

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

vowels =def {
    λ ""! true;
    λ α ⁀ β if oneVowel(α)! vowels(β);
    λ β. false
}

What is the result of oneVowel("ea")?
What is the result of oneVowel("")?
What is the result of vowels("ea")?
What is the result of vowels("eat")?

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)?
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).
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?
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 α.
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")?
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 β.
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:"?
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(":").

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(β, ":") }

What is anyOf(":a:b:c:", oneVowel)?
What is anyOf(":b:", oneVowel)?
What is anyOf(":", oneVowel)?