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

Sample answers in purple.

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).`endsWith (γ, δ) =def dissect γ { λ α ⁀ β if β = δ! true; λ β. false }`

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"`

.`anyWhere (γ, δ) =def dissect γ { λ η ⁀ α ⁀ β if α = δ! true; λ β. false }`

This counts the empty string and

`"dog"`

as both occurring inside`"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) }`

- What is the result of
`take("abc", 2)`

?`"ab"`

- What is the result of
`take("", 2)`

?`""`

- What is the result of
`take("abc", 5)`

?`"abc"`

- What is the result of
`take("abc", 0)`

?`""`

- What is the result of
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)`

.`drop (γ, x) =def dissect γ { λ β if x = 0! β; λ "". ""; λ α ⁀ β if isUnit(α). drop(β, x - 1) }`

This makes

`drop(γ, x)`

for any string whose length is`≤ x`

be`""`

.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")`

?`false`

- What is the result of
`oneVowel("")`

?`false`

- What is the result of
`vowels("ea")`

?`true`

- What is the result of
`vowels("eat")`

?`false`

- What is the result of
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.**)- What is the result of
`takeWhile1("dog", oneVowel)`

?`""`

- What is the result of
`takeWhile1("eat", oneVowel)`

?`"ea"`

- What is the result of
`takeWhile1("eat", isUnit)`

?`"eat"`

- What is the result of
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)`

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

This makes

`dropWhile1("", Q)`

for any predicate`Q`

be`""`

. It makes`dropWhile1("ea", oneVowel)`

also be`""`

.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, δ ⁀ α); λ β. δ }`

- What is the result of
`takeWhile2("dog", oneVowel, "")`

?`""`

- What is the result of
`takeWhile2("eat", oneVowel, "")`

?`"e"`

- What is the result of
`takeWhile2("eat", vowels, "")`

?

`"ea"`

One quick way to get the result is to imagine the argument

`"eat"`

being dissected on the initial application of the function`takeWhile2`

in such a way that`α`

is assigned`"ea"`

and`β`

is assigned`"t"`

. (Why should it dissect that way, you ask? Nothing forces it to do so. But if the function is not stinky, then any dissecting that satisfies the clause should deliver the same result.) This is a case where`α ≠ "" and Q("" ⁀ α)`

. So then the result will be`takeWhile2 ("t", Q, "ea")`

. Since there is no way to dissect`"t"`

where the first part is non-empty and satisfies that predicate, the result of the recursive call will be`"ea"`

.If you instead want to dissect

`"eat"`

one unit at a time, the derivation would go:`takeWhile2("eat", vowels, "") = takeWhile2("at", Q, "e") = takeWhile2("t", Q, "ea")) = "ea"`

- What is the result of
`takeWhile2("eat", isUnit, "")`

?`"e"`

;`takeWhile1("eat", isUnit)`

would be`"eat"`

; to get the same effect with`takeWhile2`

, you’d need to use a predicate like`{ λ β. true }`

- Will the result of
`takeWhile2(γ, Q, "")`

always satisfy the predicate`Q`

? If so, explain why. If not, when will this fail? case (a) is an example where it fails

- What is the result of
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`α`

.Thesis to be shown: any string with suffix

`"t"`

(that is,`δ ⁀ "t"`

for any string`δ`

) has length > 0.Base Step: We establish the thesis for the case where

`δ`

is`""`

, thusly:`"" ⁀ "t"`

=`"t"`

and by definition`length("t")`

=`1 + length("")`

=`1 + 0`

which is`> 0`

.Induction Step: We assume that the thesis has been established for the case where

`δ`

is`η`

. Allowing ourselves that assumption, we establish the claim for the case where`δ`

is`α ⁀ η`

for some unit string`α`

, thusly: by definition`length(α ⁀ η)`

if`isUnit(α)`

is`1 + length(η)`

, which by our assumption is`1 + x`

where`x`

is`> 0`

.Since we established that the thesis holds for the case where

`δ`

is`""`

, and also the case where`δ`

is`α ⁀ η`

where`α`

is a unit and`η`

is any string that the thesis has already been established for, we’ve shown that the thesis holds for any finite string`δ`

.We say that the

**reverse**of a string`"abc"`

is`"cba"`

. We can define that notion like this:`reverse =def { λ "". ""; λ α ⁀ β if isUnit(β). β ⁀ reverse(α) }`

- What is
`reverse("")`

?`""`

- What is
`reverse("t")`

?`"t"`

- What is
`reverse("abba")`

?`"abba"`

- What is
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`β`

.Thesis to be shown: for any string

`δ`

, it holds that`reverse(γ ⁀ δ) = reverse(δ) ⁀ reverse(γ)`

.Base Step: We establish the thesis for the case where

`δ`

is`""`

, thusly: because of how`""`

concatenates,`reverse(γ ⁀ "") = reverse(γ) = "" ⁀ reverse(γ)`

; and by definition`reverse("") = ""`

, so that last is`reverse("") ⁀ reverse(γ)`

.Induction Step: We assume that the thesis has been established for the case where

`δ`

is`η`

. Allowing ourselves that assumption, we establish the claim for the case where`δ`

is`η ⁀ β`

for some unit string`β`

, thusly: by definition`reverse(γ ⁀ η ⁀ β)`

if`isUnit(β)`

is`β ⁀ reverse(γ ⁀ η)`

. By our assumption, that’s equivalent to`β ⁀ reverse(η) ⁀ reverse(γ)`

. By definition`reverse(η ⁀ β)`

if`isUnit(β)`

is`β ⁀ reverse(η)`

, so that last is`reverse(η ⁀ β) ⁀ reverse(γ)`

.Similarly to Problem 64, since we established that the thesis holds for the case where

`δ`

is`""`

, and also the case where`δ`

is`η ⁀ β`

where`β`

is a unit and`η`

is any string that the thesis has already been established for, we’ve shown that the thesis holds for any finite 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(β, ":") }`

- What is
`headOf(":abc::")`

?`"abc"`

- What is
`headOf("::abc:")`

?`""`

- What is
`headOf(":")`

?`":"`

- What is
`headOf`

applied to a string that doesn’t encode a sequence according to our conventions, like`""`

or`":abc"`

or`"abc:"`

?`undefined`

- What is
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(":")`

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

This makes

`tailOf(":")`

be`":"`

.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)`

?`true`

- What is
`anyOf(":b:", oneVowel)`

?`false`

- What is
`anyOf(":", oneVowel)`

?`false`

- What is