Phil 455: Homework 5

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
}

56. 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
    }

57. 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".

58. 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)? "ab"
    2. What is the result of take("", 2)? ""
    3. What is the result of take("abc", 5)? "abc"
    4. What is the result of take("abc", 0)? ""

59. 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 "".

60. 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")? false
    2. What is the result of oneVowel("")? false
    3. What is the result of vowels("ea")? true
    4. What is the result of vowels("eat")? false

61. 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)? "ea"
    3. What is the result of takeWhile1("eat", isUnit)? "eat"

62. 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 "".

63. 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, "")? "e"
    3. 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"

    4. 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 }
    5. 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

64. 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 δ.

65. 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")? "t"
    3. What is reverse("abba")? "abba"

66. 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 δ.

67. 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::")? "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:"? undefined

68. 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 ":".

69. 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)? true
    2. What is anyOf(":b:", oneVowel)? false
    3. What is anyOf(":", oneVowel)? false