Tree Paths, isPath Predicate, and Path Sum Lemma

Overview

  • Topic: working with trees, paths, and sums along paths; defining a predicate isPath to recognize valid root-to-leaf sequences, and exploring a sum-based property (path sums) with recursive functions and a proof sketch.
  • Context: a tree with nodes containing values, and paths are sequences of values from the root to a leaf.
  • Notation used in the lecture:
    • Tree is either Empty or Node(e, L, R) where e is the root value, L is the left subtree, and R is the right subtree.
    • A path is a sequence of values [v0, v1, …, vk] that corresponds to values encountered when walking from root to a leaf.
    • A sequence is treated like an array with indexing: p0 is the first element, p1 is the second, and p tail can be written as p1.. to denote all elements except the first.
    • Equality must be defined for the type used in the sequence (type must support ==).
  • Goals:
    • Define a predicate isPath(p, t) that decides if p is a valid path in t.
    • Explain how to traverse a tree to confirm a path, including handling the empty-tree case and the non-empty case.
    • Introduce a helper function sum(p) that adds all numbers in a sequence.
    • Introduce parsesum(t, s): whether there exists a path in t whose sum equals s.
    • Present a lemma: if parsesum(t, s) holds, then there exists a path p in t such that sum(p) = s (existence, not uniqueness).
    • Sketch the inductive proof and discuss where induction hypotheses are needed and why certain steps matter.

Definition of a path in a tree

  • A path is a root-to-leaf sequence of node values in the tree.
  • Example paths in a sample tree include sequences like [14, 7, 2, 17], [14, 7], [14, 25], etc.
  • Path formalization goal: given a sequence p and a tree t, determine if p corresponds to a valid root-to-leaf path of t.
  • Predicate type: isPath : Seq a -> Tree a -> Bool, requiring a type a that supports equality (==).
  • Type requirements:
    • The element type a must have equality defined so we can compare p[0] with the root value e.
    • If you define a custom type for which == isn’t provided, you must implement equality accordingly (not covered in depth here).

isPath: base cases and recursive structure

  • Base case (empty tree):
    • For an empty tree, the only valid path is the empty sequence.
    • Formally: extisPath(p,extEmpty)extholdsextiffp=[]ext{isPath}(p, ext{Empty}) ext{ holds } ext{iff } p = []
  • Non-empty case (node with value e and subtrees L, R):
    • If p is non-empty, let p0 be the first element and ptail be the remainder: p = [p0] ulllisttail.
    • We must have p0 = e (root matches the first element of the path).
    • Then the remainder p_tail must be a valid path in either the left subtree L or the right subtree R.
    • Formalized with recursion:
    • ext{isPath}([p0] ull p{ ext{tail}}, ext{Node}(e,L,R)) ext{ holds } \
      ext{iff } p0 = e \,\land\, ( ext{isPath}(p{ ext{tail}}, L) \,\lor\, ext{isPath}(p_{ ext{tail}}, R))
  • Note: The lecture uses notation like p0 for the first element and p1 . . for the tail, and checks both left and right subtrees recursively with the reduced path.

Working through the empty-tree and non-empty-tree cases

  • Empty tree case intuition:
    • If you have an empty path, it’s valid for an empty tree.
    • If you have any non-empty path, it cannot be a path in an empty tree.
  • Non-empty tree case intuition:
    • You compare the path’s first element with the root value and then decide which subtree (left or right) might continue the path.
    • If both subtrees fail to yield a match for the tail, the overall path is invalid.
  • Practical notes:
    • The check is performed by pattern matching on the tree, then matching the first element of the path with the node value, followed by a recursive check on either the left or right subtree using the tail of the path (p tail).
    • The order of trying left vs right is not fixed; either may yield success depending on the path.

Left/right recursion and the path-check mechanism

  • At each non-empty node (e, L, R) with path p = [p0, p1, …], after validating p0 = e, we recursively test:
    • isPath(ptail, L) or isPath(ptail, R)
  • The tail p_tail is obtained as p[1..], i.e., everything after the first element.
  • This leads to a branching search: the correct path could be found entirely in the left subtree or entirely in the right subtree.
  • Example reasoning snippet:
    • If you try the right subtree first and it fails, you backtrack and try the left subtree with the same tail.
    • If a valid path exists following the left subtree, you’ll eventually reach a leaf with an empty tail and the left path succeeds; similar for the right subtree.

A simple sanity check (lemma) for isPath with empty input

  • Toy example: isPath with an empty path and an empty tree should yield true.
  • Example: isPath([], IntTree) with an empty tree type Int should return true; with non-empty tree it would return false unless the path matches a root-to-leaf path, which would require at least a single element equal to the root.

Sum of a sequence (helper function)

  • Purpose: to sum all numbers in a path sequence.
  • Definition as a recursive function on a Seq of numbers:
    • Base case: extsum(p)=0extifp=[]ext{sum}(p) = 0 ext{ if } p = []
    • Recursive case: if p = [p0] ull p{ ext{tail}}, then extsum(p)=p<em>0+extsum(p</em>exttail)ext{sum}(p) = p<em>0 + ext{sum}(p</em>{ ext{tail}})
  • This is a straightforward recursion stepping through the path values from left to right until the sequence is exhausted.

The parsesum function: existence of a path with a given sum

  • Goal: Given a tree of integers T and an integer s, decide whether there exists a path through T whose values sum to s.
  • Function signature (informally): parsesum(T, s) : Bool
  • Base case (empty tree):
    • If T = Empty, only the empty path contributes a sum of 0, so
    • extparsesum(extEmpty,s)=(s=0)ext{parsesum}( ext{Empty}, s) = (s = 0)
  • Non-empty case (node with value e, left L, right R):
    • A path through T either continues through L or through R after consuming the root value e.
    • The remaining sum is s - e.
    • Therefore:
    • extparsesum(extNode(e,L,R),s)=extparsesum(L,s−e)∨parsesum(R,s−e)ext{parsesum}( ext{Node}(e,L,R), s) = ext{parsesum}(L, s - e) \lor \text{parsesum}(R, s - e)
  • Intuition: you subtract the current node’s value from the target sum and ask whether the remainder can be achieved in one of the subtrees.
  • Example interpretation (in words): if you want a path that sums to s, you can either extend a left-subtree path with the current root, or extend a right-subtree path with the current root.

Lemma: existence of a path from parsesum (path-sum implies a path exists)

  • Formal statement:
    • For a tree T of integers and a sum s, if \text{parsesum}(T, s) holds, then there exists a path p in T such that isPath(p, T) and sum(p) = s.
    • Symbolically: extparsesum(T,s)⇒∃p (extisPath(p,T)∧sum(p)=s).ext{parsesum}(T, s) \Rightarrow \exists p \, ( ext{isPath}(p, T) \land \text{sum}(p) = s ).
  • This is the key existential claim: a successful path-sum predicate guarantees at least one concrete path achieving the sum.
  • Conceptual translation: if there exists a way to split the problem down to a sub-tree with s - e, IH gives you an actual path in that sub-tree, then prepending e to that path yields a valid path in the original tree with sum s.

Inductive proof sketch for the lemma

  • Setup: prove by induction on the structure of the tree.
  • Base case: T = Empty
    • parsesum(Empty, s) holds only when s = 0.
    • The corresponding path is the empty sequence [] with sum 0, so there exists a path (the empty path) achieving sum s = 0.
    • Therefore the claim holds: there exists a path p (the empty path) with isPath(p, Empty) and sum(p) = s.
  • Inductive step: T = Node(e, L, R)
    • Inductive hypothesis (IH): assume the lemma holds for L and for R for all smaller sums.
    • If parsesum(Node(e,L,R), s) holds, then by the definition above, either parsesum(L, s - e) or parsesum(R, s - e) holds.
    • Case 1: parsesum(L, s - e) holds. By IH for L, there exists a path pL in L with isPath(pL, L) and sum(pL) = s - e. Then the concatenated path p = [e] ++ pL is a valid path in Node(e,L,R) with sum(p) = e + (s - e) = s, and isPath(p, Node(e,L,R)) holds (root matches, and path continues into L).
    • Case 2: parsesum(R, s - e) holds. By IH for R, there exists a path pR in R with isPath(pR, R) and sum(pR) = s - e. Then p = [e] ++ pR is a valid path in Node(e,L,R) with sum(p) = s, and isPath(p, Node(e,L,R)) holds (root matches, and path continues into R).
    • In either case, a witness path exists, establishing the existential claim for Node(e,L,R).
  • Remarks on the role of IH in the proof:
    • The speaker notes that removing the inductive-hypothesis-related lines can cause the proof to fail to establish the required existence, because the proof relies on constructing a concrete path from the sub-tree path witness.
    • Some minor reformulations (e.g., naming the witnesses PL and PR and then lifting them back to a path in the full tree) are used to illustrate the constructive step.
    • In some attempts, the proof may still be valid by the automated prover (depending on settings), but the explicit IH-guided witness construction makes the argument robust.

Connections and practical implications

  • Connections to foundational principles:
    • Induction on data structure (trees) as a standard proof technique for recursive predicates like isPath and parsesum.
    • Use of base cases (empty tree) and inductive steps (node with subtrees) mirrors structural recursion.
    • The sum operation is a simple reduction that enables a path-sum problem to be transformed into a subproblem with a reduced target sum (s - e).
  • Real-world relevance:
    • Path detection in trees is a common operation in parsing, decision trees, and search problems.
    • Path-sum problems resemble subset-sum-like problems but constrained to tree paths, which often have tractable recursive structure.
  • Philosophical/practical implications:
    • The distinction between “exists a path with sum s” and “parsesum returns true” highlights constructive proofs: parsesum serves as a certificate that such a path exists, and the IH steps provide a constructive witness.
    • Equality constraints (typeclass or operator ≡) matter for user-defined types; the code requires a well-defined equality operator to perform the root-value comparison.

Numerical example (illustrative; not tied to exact numbers in the talk)

  • Suppose a path p = [e, …, …] has elements that sum to s; parsesum(T, s) should return true.
  • If parsesum(T, s) returns true via the L-subtree path with remainder s - e, then the witness path is p = [e] ++ pL, where pL sums to s - e.
  • If the path leads through the right subtree, the witness path is p = [e] ++ pR with pR summing to s - e.

Summary of key ideas

  • Path concept: sequences from the root to a leaf that align with the tree’s structure.
  • isPath predicate: checks first element against root, then recursively checks left or right subtree with the tail of the sequence.
  • Sum and parsesum: sum computes the total along a path; parsesum checks for the existence of a path whose sum equals a target s.
  • Lemma and its proof: parsesum implies the existence of an actual path with the given sum, proven by induction on the tree and constructive witnesses from subtrees.
  • Practical considerations: induction hypotheses are essential for constructing the witness path; removing critical lines can break the proof.

Next steps and instructor notes

  • The instructor mentions mini-assignments, feedback on quizzes, and a transition to another example next session.
  • This material sets the basis for more advanced tree-path reasoning and proofs, possibly including more complex data types and additional predicates.