Проверка LeetCode Вопрос: 112. Сумма путей

Давайте посмотрим на проблема определение.

Учитывая корень двоичного дерева и целое число targetSum, вернуть true, если дерево имеет путь от корня к листу, такой что суммирование всех значений на пути равно targetSum.

Лист — это узел без потомков.


Реализация

Вот как мы можем решить это в JavaScript/TypeScript.

function hasPathSum(root: TreeNode | null, targetSum: number): boolean {
    if(root == null) {
        return false;
    }
    if(root.val-targetSum == 0 && root.left == null && root.right == null) {
        return true;
    }
    return hasPathSum(root.left, targetSum-root.val) || hasPathSum(root.right, targetSum-root.val);
};
Войти в полноэкранный режим

Выйти из полноэкранного режима

Проблемы с деревьями часто легко решаются с помощью рекурсивного алгоритма.

Разбивая это по случаям:
если текущий корень равен нулю, то нет пути, соответствующего targetSum.

если значение текущего узла соответствует targetSum, а текущий узел является конечным узлом, то все готово, путь существует.

Если есть путь в левом дочернем текущем узле или если есть путь в правом дочернем текущем узле минус текущее значение этого узла, то путь существует.


Указание реализации

Сначала мы определяем тип данных дерева.

datatype TreeNode = Nil | Tree(val: nat, left: TreeNode, right: TreeNode)
Войти в полноэкранный режим

Выйти из полноэкранного режима

Мы переводим определение проблемы в две вспомогательные функции/предикаты. В Dafny, тип последовательности, seq является типом массива, подобного объекту (т.е. он может быть проиндексирован), а также похож на связанный список. assert path == [path[0]+path[1..];

predicate isPath(paths: seq<TreeNode>, root: TreeNode) {
    if |paths| == 0 then false else match paths[0] {
        case Nil => false
        case Tree(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))
    }
}
Войти в полноэкранный режим

Выйти из полноэкранного режима

Мы говорим, что путь — это последовательность TreeNodes, начинающаяся с корня. Тогда, если последовательность не пуста и первый узел не Nil, а корень равен первому узлу в списке, то если остальная часть списка (удаление первого элемента/корня) является либо путем, начинающимся с корней левый ребенок или правый ребенок. Он вернет true или false, если это правильный путь в дереве.

function pathSum(paths: seq<TreeNode>): nat {
    if |paths| == 0 then 0 else match paths[0] {
        case Nil => 0
        case Tree(val, left, right) => val + pathSum(paths[1..])
    }
}
Войти в полноэкранный режим

Выйти из полноэкранного режима

Учитывая путь, мы рекурсивно разбиваем список на первый элемент и остальную часть списка, а затем добавляем значение узла к pathSum остальной части списка.

Учитывая эти определения, мы можем перевести определение проблемы следующим образом:

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
}
Войти в полноэкранный режим

Выйти из полноэкранного режима

Опять же, мы можем проверить существование некоторого пути p, который суммируется с targetSum, если метод возвращает true.


Проверка реализации

Это должно быть простое преобразование кода TypeScript в Dafny.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    return leftPath || rightPath;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима


доказательство индукции в Дафни

Когда мы пишем этот метод, Дафни не сразу убеждается в нашем предложении обеспечить. Убедиться в этом не так уж сложно, но мы должны использовать еще одну особенность Дафни.

сначала разрешив конечный случай.

if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
  assert isPath([root], root) && pathSum([root]) == targetSum;
  return true;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима

Добавим утверждение, показывающее, что [root] является допустимым путем, и он существует. Во-вторых, если корневое значение == targetSum, то pathSum([root]) также равно targetSum.

После этого Дафни одобрит условие возврата, но потом пожалуется на рекурсивный случай.

Мы вызываем рекурсивные вызовы и сохраняем результат в переменную, затем разбиваем его на случаи.

var leftPath := hasPathSum(root.left, targetSum-root.val);
var rightPath := hasPathSum(root.right, targetSum-root.val);

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}
if rightPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима

Новый синтаксис здесь — это переменная-призрак. Ghost var — это переменная, которую Дафни может использовать для отслеживания данных, полезных для утверждений, но на самом деле она не является частью кода, который фактически запускается при запуске метода.

Это переменная, которая существует только в контексте спецификации, а не в контексте выполнения программы.

Во-вторых, мы используем :| смысл оператора such thatтак что в основном мы можем прочитать следующее утверждение так.

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима

Если переменная leftPath имеет значение true, то индуктивно hasPathSum говорит, что существует путь p, начинающийся в корневом левом узле, и его сумма путей равна targetSum-root.val. Мы назначаем этот путь p. Затем мы показываем, что если мы добавим корень к этому пути, то это все еще будет допустимым путем, а pathSum будет root.val+(targetSum-root.val) == targetSum. После того же аргумента справа метод проверяет.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        assert isPath([root], root) && pathSum([root]) == targetSum;
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    if leftPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    if rightPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    return leftPath || rightPath;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима