Defining a recursive function (structural induction)

Question

A list of integers can be recursively defined as follows:

<IntList> ::= [] | cons(<Int>, <IntList>)

Write a recursive function named allEqualTo that takes an integer and a list as input, and returns 1 if all the numbers in the list are equal to the given integer, and 0 otherwise. For example, allEqualTo(5, cons(5, cons(5, []))) should return 1, and allEqualTo(5, cons(5, cons(3, cons(5, [])))) should return 0.

NOTE: Write a function, not a Prolog predicate or code in any other language. Feel free to use pattern matching.

This is what I did and when I checked answers, they did it in a totally different way, but I am still not convinced this is wrong, so I’m asking here.

allEqualTo(x, []) = 0
allEqualTo(x, cons(x, [])) = 1
allEqualTo(x, cons(y, a)) = 0
allEqualTo(x, cons(x, a)) = cons(x, allEqualTo(x, cons(x, a))

Edit: The solution looks like:

allEqualTo(x, []) = 0
allEqualTo(x, cons(x, [])) = 1
allEqualTo(x, cons(y, a)) = 0 x≠y 
allEqualTo(x, cons(x, a)) = allEqualTo(x, L)

Answer 1

• The last case of your function doesn't type: you are returning a list (with both an integer and booleans ---morally speaking) but allEqualTo returns an integer.
• allEqualTo(x,[]) should equal 1: indeed every element in the list is equal to x.
• I'm going to write cons with infix notation cons(x,xs) ≡ x :: xs.
• I don't know the details of the syntax of your language (you didn't provide one) but you should be able to translate anything I write.

---

Consider functions and : Int → Int → Int and infix (==) : Int → Int → Int that behave like their corresponding bool-valued versions but with 0 instead of False and 1 instead of True.

Given an integer x and a list a :: b :: c :: [] you want to return 1 if a = b = c = x and 0 otherwise.

Notice that if you map the [] to 1 and the (::) to the function λy,b. x == y and b, you would map the last list to the int

x == a and (x == b and (x == c and 1))

which is what we want. If you have a fold implemented you can write up to currying

allEqualTo x := fold 1 (λy,b. x == y and b)

where fold : ∀a,b. b → (a → b → b) → [a] → b.

---

If you want a construction with pattern matching you can unfold this definition (up to currying) to get

allEqualTo(x, [])    = 1
allEqualTo(x, y::xs) = x == y and allEqualTo(x, xs)

---

Notice here it's key that allEqualTo(x, []) = 1 since otherwise when you get to the end of the list you'll always return 0.

Also this maps the unit of the list to the ("multiplicative" -- and) unit of the booleans, and since it's the and what you are using for the recursive case, this makes your allEqualTo an algebra morphism. Doing otherwise would be unnatural.

Here's a nice introduction to the topic of $F$-algebras. Although it might require some extra reading beforehand.

Ask anything, hope this helps!