初探算法题目形式化

声明

本人不会 Lisp，以下内容纯属娱乐。

目标

使用包含依值类型的 Lisp 方言将 Codeforces 上的算法题形式化。

力求保留题意，不在形式化时进行算法优化。这样可以解耦形式化和计算。

语言特性

nat 表示自然数，lambda，vec，eq 都是类型构造函数。

nth 是由 vec 实例和 nat 实例构造 nat 实例的构造函数。

same 是构造 eq 实例的构造函数，(: i nat) 用于标注 i 的类型是 nat。

map 的使用较为灵活，例如以下函数的值是 (tuple (eq i i) ... (eq i i))，类别是 type：

(tupleMap (: dim nat)
  (lambda
    (: i nat)
    (eq i i)))

以下函数的值则是 (cons (same i i) ... (same i i))，类别是 (tuple (eq i i) ... (eq i i))：

(consMap (: dim nat)
  (lambda
    (: i nat)
    (same i i)))

对于其他形式的 map，例如 vecMap，容易猜测出其用途。

题目

来源：Codeforces Round #844 A. Parallel Projection

长方体盒子里天花板和地上选定两点，找连接这两点的最短线。要求：

• 线必须与长方体的轴平行
• 线必须贴着长方体的边

两点水平面坐标为 $(f,g),(a,b)(f,\; g),\; (a,\; b)$，矩形大小为 $(w,d)(w,\; d)$，其中 $ww$ 是宽度。

本题形式化

(define point
  (lambda
    (: dim nat)
    (vec nat dim)))
(define route
  (lambda
    (: dim nat)
    (: numPoint nat)
    (vec (point dim) numPoint)))
(define pointParallel
  (lambda
    (: dim nat)
    (: a (point dim))
    (: b (point dim))
    (geq 1
      (sum
        (vecMap nat dim
          (lambda
            (: i nat)
            (if
              (eq
                (nth a i)
                (nth b i))
              0 1)))))))
(define pointDist
  (lambda
    (: dim nat)
    (: a (point dim))
    (: b (point dim))
    (sqrt
      (sum
        (vecMap nat dim
          (lambda
            (: i nat)
            (square
              (abs
                (sub
                  (nth a i)
                  (nth b i))))))))))
(define routeParallel
  (lambda
    (: dim nat)
    (: numPoint-1 nat)
    (: route (route dim (add 1 numPoint-1)))
    (tupleMap numPoint-1
      (lambda
        (: i nat)
        (pointParallel dim
          (nth route i)
          (nth route (add 1 i)))))))
(define routeLength
  (lambda
    (: dim nat)
    (: numPoint-1 nat)
    (: route (route dim (add 1 numPoint-1)))
    (sum
      (pointDist
        (nth route i)
        (nth route (add 1 i))))))
(define routeOnPlane TODO)
(define existAns
  (tuple
    (: numPoint-1 nat)
    (: route (route 3 (add 1 numPoint-1)))
    (func
      (: i nat)
      (: r (route 3 (add 1 i)))
      (: condition
        (tuple
          (routeParallel 3 numPoint-1 route)
          (routeOnPlane 3 numPoint-1 route)
          (routeParallel 3 i r)
          (routeOnPlane 3 i r)))
      (leq
        (routeLength 3 numPoint-1 route)
        (routeLength 3 i r)))))

目标是构造出 existAns 的一个实例，其构建后容易获得回答问题所需的信息。

形式化保证了这个实例包含的信息合法。