李嘉图 Jiatu Li

I am an undergraduate student in Institute for Interdisciplinary Information Science, Tsinghua University. My research interest is about circuit complexity, pseudorandomness and the connection between complexity and cryptography. I’m also interested in the application of formal method in mathematics (i.e. computer-aided mathematics) and logic in computer science.

• Email: lijt19@mails.tsinghua.edu.cn

Publications

• Formalization of PAL·S5 in Proof Assistant, ArXiv (2020).
• $3.1n - o(n)$ Circuit Lower Bounds for Explicit Functions, ECCC (2021). A joint work with Tianqi Yang.

这个页面记录参与 NOI 系列赛及 OI 相关比赛命题的经历。

Abstract: In this work, we provide a quick introduction to the classical results about propositional logic, first-order logic, proof system and (basic) model theory, for the readers who are familiar with (informal) set theory and logic. We will cover the completeness theorem of first-order logic, the compactness theorem, Tarski’s undefinability theorem and Gödel’s incompleteness theorem, and is suitable for mathematics or computer science students who are interested in mathematical logic.

概述：本文将介绍如何实现一个非常简单的命题逻辑定理证明器。这个定理证明器用 Haskell 编写，以交互式的方式进行使用，输出 Hilbert Style System 下原命题的一个证明。用这个小工具，我们可以生成许多难以直接证明的定理（如析取、合取的结合律）的证明。

简单类型 λ 演算

简单类型 λ 演算是一种非常简单的类型系统。在本文中，我们将从简单类型 λ 演算的基本性质出发，介绍四个不那么平凡的结果：

• 强正则定理：简单类型 λ 演算中，不存在以有类型的项开始的无限长的 β 规约序列；
• 类型推导算法：对于 Curry 风格（变量不注明类型）的 λ 演算，存在高效的算法求出 λ 项的“主类型”；
• 组合子逻辑：一个仅用 2 个组合子和组合子应用形成的演算系统，不需要任何变量；
• Curry-Howard 同构：简单类型 λ 演算与直觉主义命题逻辑的自然演绎系统对应，简单类型组合子逻辑与直觉主义希尔伯特公理系统对应。

摘要：程序设计题目是目前信息学竞赛主要的教学、训练方式。本文从程序设计题目在信息学竞赛教学中的不足出发，通过分析传统的教学模式，探讨了非程序设计题目在信息学竞赛教学中的应用价值。此外，通过引入阶段性模型提出了面向教学目标的非程序设计题目设计方法，总结出一些有效的非程序设计题目形式。本文认为，非程序设计题目作为传统程序设计题目训练的补充，可以在缺乏教师指导的情况下提升整体教学效果，是一种值得推广的教学设计方法。

关键词：信息学竞赛教育，教学方法，教学研究，非程序设计题目

概述

k-sorter 问题指如何利用“给 k 个元素排序”这一基本操作，构造高效的排序算法。由于一个 k-sorter 可以由 $k\log k$ 次比较操作构造，而比较排序的时间复杂度下界是 $n\log n$，因此 k-sorter 问题的排序器使用次数下界（下称比较下界）为 $n\log n/k\log k$。我对这个问题的了解来自于清华大学邓俊辉老师的《数据结构》课程中的一道编程练习题（题目对应 $k=3$ 的情景），并将一个简单的做法（$n\log n/k$ 次比较的算法）出做了集训队作业题目¹。近期我对此问题又做了一些调查和探索，结论如下：

• 存在若干种比较次数在 $O(n\log n/k)$ 的确定性排序算法，包括两个比较简单的基于归并的算法；
• 存在期望 $O(n\log n/k\log k)$ 次比较的随机算法，这一算法思路简单，但分析稍加繁琐；
• 存在 $(n\log n/k\log k)$ 次比较的确定性算法，这一算法来自².

$k$ 祖先问题

$k$ 祖先问题（Level Ancestor Problem）是静态树的重要问题之一。给定一棵树和若干个询问 $(u, k)$，要求结点 $u$ 的第 $k​$ 个祖先结点。

离线情景下的 $k$ 祖先问题存在一个简单的 $O(n+q)$ 的算法：在 dfs 的过程中维护一个记录祖先的栈，然后在每个结点处回答和这个结点有关的所有询问；在线情景下有基于倍增的 $O(n\log n)-O(\log n)$ 算法，基于长链剖分的 $O(n)-O(\log n)$ 算法和 $O(n\log n) - O(1)$ 算法，以及最终的 $O(n) - O(1)$ 算法。

缓存无关模型

在算法层面考虑储存器层次结构时，我们通常使用的是外部储存模型（External Memory Model）。在这样的模型中，储存器具有两级 $L_1, L_2$，且 $|L_1| = M, |L_2| = \infty$。$L_1$ 被看作 $L_2$ 的缓存，当访问的数据不在 $L_1$ 中时，我们将数据从 $L_2$ 中调入 $L_1$，并花费 $T$ 的传输时间。

Stage0

某天深夜水群的时候给小朋友普及 Tarjan 算法求 LCA 的时间复杂度，被老鸽们指正应当是 $O(n+q)$ 而非$O((n+q)\alpha(n))$。最近阅读了一下 wiki 上指出的论文 ¹ 学习了一下。

先放结论：RMQ 问题和 LCA 问题的最优复杂度都是 $O(n)-O(1)$ 的，线性复杂度的 Tarjan 需要做一些操作。