From 72f1ce9168640252abf8e4aefb379ced2ce48b1f Mon Sep 17 00:00:00 2001 From: yhtq <1414672068@qq.com> Date: Thu, 17 Oct 2024 10:16:59 +0800 Subject: [PATCH] 10.17 --- .VSCodeCounter/2024-10-17_10-15-14/details.md | 119 +++++++ .../2024-10-17_10-15-14/diff-details.md | 15 + .VSCodeCounter/2024-10-17_10-15-14/diff.csv | 2 + .VSCodeCounter/2024-10-17_10-15-14/diff.md | 19 ++ .VSCodeCounter/2024-10-17_10-15-14/diff.txt | 22 ++ .../2024-10-17_10-15-14/results.csv | 106 +++++++ .../2024-10-17_10-15-14/results.json | 1 + .VSCodeCounter/2024-10-17_10-15-14/results.md | 61 ++++ .../2024-10-17_10-15-14/results.txt | 168 ++++++++++ template.typ | 3 + .../main.typ" | 3 +- ...3\345\215\212\345\255\246\346\234\237.typ" | 12 +- .../main.typ" | 23 ++ .../main.typ" | 67 +++- .../\344\275\234\344\270\232/ml-2_2-hw.typ" | 112 +++++++ .../\344\275\234\344\270\232/ml-3_1-hw.typ" | 83 +++++ .../main.typ" | 178 ++++++++++- .../\344\275\234\344\270\232/hw3.typ" | 124 ++++++++ .../code/hw2/hw2.typ" | 101 ++++++ .../main.typ" | 132 ++++++++ ...4\346\254\241\344\275\234\344\270\232.typ" | 77 +++++ .../main.typ" | 300 +++++++++++++----- 22 files changed, 1634 insertions(+), 94 deletions(-) create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/details.md create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/diff-details.md create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/diff.csv create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/diff.md create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/diff.txt create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/results.csv create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/results.json create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/results.md create mode 100644 .VSCodeCounter/2024-10-17_10-15-14/results.txt create mode 100644 "\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-2_2-hw.typ" create mode 100644 "\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-3_1-hw.typ" create mode 100644 "\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/\344\275\234\344\270\232/hw3.typ" create mode 100644 "\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw2/hw2.typ" create mode 100644 "\350\275\257\344\273\266\345\210\206\346\236\220/hw/2100012990-\351\203\255\345\255\220\350\215\200-\350\275\257\345\210\206\347\254\254\344\272\224\346\254\241\344\275\234\344\270\232.typ" diff --git a/.VSCodeCounter/2024-10-17_10-15-14/details.md b/.VSCodeCounter/2024-10-17_10-15-14/details.md new file mode 100644 index 0000000..6bbe7fa --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/details.md @@ -0,0 +1,119 @@ +# Details + +Date : 2024-10-17 10:15:14 + +Directory /home/yhtq/学习/课程 + +Total : 104 files, 39765 codes, 706 comments, 1463 blanks, all 41934 lines + +[Summary](results.md) / Details / [Diff Summary](diff.md) / [Diff Details](diff-details.md) + +## Files +| filename | language | code | comment | blank | total | +| :--- | :--- | ---: | ---: | ---: | ---: | +| [template.typ](/template.typ) | Typst | 403 | 122 | 31 | 556 | +| [typst-sympy-calculator.typ](/typst-sympy-calculator.typ) | Typst | 69 | 3 | 11 | 83 | +| [代数学二/main.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/main.typ) | Typst | 10 | 2 | 0 | 12 | +| [代数学二/习题课.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%B9%A0%E9%A2%98%E8%AF%BE.typ) | Typst | 384 | 2 | 2 | 388 | +| [代数学二/作业/hw1.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw1.typ) | Typst | 215 | 2 | 4 | 221 | +| [代数学二/作业/hw10.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw10.typ) | Typst | 172 | 0 | 8 | 180 | +| [代数学二/作业/hw11.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw11.typ) | Typst | 97 | 0 | 5 | 102 | +| [代数学二/作业/hw12.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw12.typ) | Typst | 218 | 0 | 4 | 222 | +| [代数学二/作业/hw2.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw2.typ) | Typst | 259 | 2 | 4 | 265 | +| [代数学二/作业/hw3.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw3.typ) | Typst | 335 | 23 | 7 | 365 | +| [代数学二/作业/hw4.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw4.typ) | Typst | 253 | 15 | 13 | 281 | +| [代数学二/作业/hw5.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw5.typ) | Typst | 291 | 11 | 6 | 308 | +| [代数学二/作业/hw6.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw6.typ) | Typst | 480 | 0 | 8 | 488 | +| [代数学二/作业/hw7.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw7.typ) | Typst | 119 | 0 | 6 | 125 | +| [代数学二/作业/hw8.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw8.typ) | Typst | 331 | 1 | 5 | 337 | +| [代数学二/作业/hw9.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw9.typ) | Typst | 255 | 0 | 12 | 267 | +| [代数学二/章节/test.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E7%AB%A0%E8%8A%82/test.typ) | Typst | 0 | 0 | 1 | 1 | +| [代数学二/章节/上半学期.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E7%AB%A0%E8%8A%82/%E4%B8%8A%E5%8D%8A%E5%AD%A6%E6%9C%9F.typ) | Typst | 3,111 | 11 | 74 | 3,196 | +| [代数学二/章节/下半学期.typ](/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E7%AB%A0%E8%8A%82/%E4%B8%8B%E5%8D%8A%E5%AD%A6%E6%9C%9F.typ) | Typst | 2,455 | 2 | 45 | 2,502 | +| [几何学/main.typ](/%E5%87%A0%E4%BD%95%E5%AD%A6/main.typ) | Typst | 2,646 | 10 | 123 | 2,779 | +| [复变函数/main.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/main.typ) | Typst | 2,358 | 4 | 46 | 2,408 | +| [复变函数/作业/hw1.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw1.typ) | Typst | 102 | 2 | 8 | 112 | +| [复变函数/作业/hw10.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw10.typ) | Typst | 65 | 2 | 0 | 67 | +| [复变函数/作业/hw2.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw2.typ) | Typst | 120 | 2 | 3 | 125 | +| [复变函数/作业/hw3.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw3.typ) | Typst | 87 | 2 | 1 | 90 | +| [复变函数/作业/hw4.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw4.typ) | Typst | 108 | 2 | 1 | 111 | +| [复变函数/作业/hw5.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw5.typ) | Typst | 56 | 2 | 2 | 60 | +| [复变函数/作业/hw6.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw6.typ) | Typst | 46 | 2 | 0 | 48 | +| [复变函数/作业/hw7.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw7.typ) | Typst | 91 | 2 | 0 | 93 | +| [复变函数/作业/hw8.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw8.typ) | Typst | 321 | 2 | 6 | 329 | +| [复变函数/作业/hw9.typ](/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw9.typ) | Typst | 81 | 2 | 1 | 84 | +| [常微分方程/main.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/main.typ) | Typst | 2,911 | 8 | 37 | 2,956 | +| [常微分方程/作业/2100012990 郭子荀 常微分方程 3.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%203.typ) | Typst | 341 | 9 | 4 | 354 | +| [常微分方程/作业/2100012990 郭子荀 常微分方程 4.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%204.typ) | Typst | 194 | 2 | 2 | 198 | +| [常微分方程/作业/2100012990 郭子荀 常微分方程 5.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%205.typ) | Typst | 135 | 2 | 2 | 139 | +| [常微分方程/作业/2100012990 郭子荀 常微分方程 6.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%206.typ) | Typst | 132 | 2 | 3 | 137 | +| [常微分方程/作业/2100012990 郭子荀 常微分方程 7.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%207.typ) | Typst | 340 | 2 | 6 | 348 | +| [常微分方程/作业/2100012990 郭子荀 常微分方程 8.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%208.typ) | Typst | 256 | 2 | 5 | 263 | +| [常微分方程/作业/hw1.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/hw1.typ) | Typst | 345 | 8 | 5 | 358 | +| [常微分方程/作业/hw2.typ](/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/hw2.typ) | Typst | 568 | 7 | 7 | 582 | +| [并行与分布式计算/main.typ](/%E5%B9%B6%E8%A1%8C%E4%B8%8E%E5%88%86%E5%B8%83%E5%BC%8F%E8%AE%A1%E7%AE%97/main.typ) | Typst | 140 | 0 | 3 | 143 | +| [抽象代数/main.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/main.typ) | Typst | 13 | 6 | 2 | 21 | +| [抽象代数/作业/hw10.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw10.typ) | Typst | 719 | 36 | 12 | 767 | +| [抽象代数/作业/hw11.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw11.typ) | Typst | 228 | 12 | 3 | 243 | +| [抽象代数/作业/hw12.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw12.typ) | Typst | 324 | 2 | 5 | 331 | +| [抽象代数/作业/hw2.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw2.typ) | Typst | 111 | 2 | 3 | 116 | +| [抽象代数/作业/hw3.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw3.typ) | Typst | 598 | 37 | 73 | 708 | +| [抽象代数/作业/hw4.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw4.typ) | Typst | 237 | 2 | 6 | 245 | +| [抽象代数/作业/hw5.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw5.typ) | Typst | 344 | 28 | 6 | 378 | +| [抽象代数/作业/hw6.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw6.typ) | Typst | 194 | 2 | 27 | 223 | +| [抽象代数/作业/hw7.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw7.typ) | Typst | 654 | 99 | 22 | 775 | +| [抽象代数/作业/hw8.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw8.typ) | Typst | 460 | 30 | 10 | 500 | +| [抽象代数/作业/hw9.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw9.typ) | Typst | 232 | 2 | 13 | 247 | +| [抽象代数/章节/模、域.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E7%AB%A0%E8%8A%82/%E6%A8%A1%E3%80%81%E5%9F%9F.typ) | Typst | 1,414 | 0 | 15 | 1,429 | +| [抽象代数/章节/环.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E7%AB%A0%E8%8A%82/%E7%8E%AF.typ) | Typst | 795 | 0 | 29 | 824 | +| [抽象代数/章节/群论.typ](/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E7%AB%A0%E8%8A%82/%E7%BE%A4%E8%AE%BA.typ) | Typst | 1,186 | 0 | 238 | 1,424 | +| [数学模型/main.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/main.typ) | Typst | 2,443 | 3 | 50 | 2,496 | +| [数学模型/作业/hw2.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw2.typ) | Typst | 328 | 9 | 5 | 342 | +| [数学模型/作业/hw3.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw3.typ) | Typst | 158 | 2 | 4 | 164 | +| [数学模型/作业/hw4.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw4.typ) | Typst | 37 | 2 | 0 | 39 | +| [数学模型/作业/hw5.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw5.typ) | Typst | 139 | 9 | 3 | 151 | +| [数学模型/作业/hw6.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw6.typ) | Typst | 109 | 6 | 4 | 119 | +| [数学模型/作业/hw7.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw7.typ) | Typst | 166 | 2 | 3 | 171 | +| [数学模型/论文/pkuthss-typst/changelog.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/changelog.typ) | Typst | 80 | 0 | 35 | 115 | +| [数学模型/论文/pkuthss-typst/contributors.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/contributors.typ) | Typst | 4 | 0 | 2 | 6 | +| [数学模型/论文/pkuthss-typst/template.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/template.typ) | Typst | 663 | 107 | 77 | 847 | +| [数学模型/论文/pkuthss-typst/thesis.typ](/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/thesis.typ) | Typst | 923 | 5 | 30 | 958 | +| [数理逻辑/main.typ](/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/main.typ) | Typst | 484 | 0 | 10 | 494 | +| [数理逻辑/作业/ml-1_1-hw.typ](/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-1_1-hw.typ) | Typst | 141 | 0 | 6 | 147 | +| [数理逻辑/作业/ml-1_2-hw.typ](/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-1_2-hw.typ) | Typst | 165 | 0 | 3 | 168 | +| [数理逻辑/作业/ml-2_1-hw.typ](/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-2_1-hw.typ) | Typst | 214 | 1 | 8 | 223 | +| [数理逻辑/作业/ml-2_2-hw.typ](/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-2_2-hw.typ) | Typst | 112 | 0 | 0 | 112 | +| [数理逻辑/作业/ml-3_1-hw.typ](/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-3_1-hw.typ) | Typst | 81 | 0 | 2 | 83 | +| [机器学习数学导引/main.typ](/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/main.typ) | Typst | 286 | 0 | 8 | 294 | +| [机器学习数学导引/作业/hw1.typ](/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/%E4%BD%9C%E4%B8%9A/hw1.typ) | Typst | 84 | 0 | 6 | 90 | +| [机器学习数学导引/作业/hw2.typ](/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/%E4%BD%9C%E4%B8%9A/hw2.typ) | Typst | 241 | 0 | 3 | 244 | +| [机器学习数学导引/作业/hw3.typ](/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/%E4%BD%9C%E4%B8%9A/hw3.typ) | Typst | 120 | 0 | 5 | 125 | +| [经济学原理/hw/hw10.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw10.typ) | Typst | 104 | 0 | 0 | 104 | +| [经济学原理/hw/hw11.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw11.typ) | Typst | 150 | 0 | 1 | 151 | +| [经济学原理/hw/hw12.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw12.typ) | Typst | 83 | 0 | 1 | 84 | +| [经济学原理/hw/hw13.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw13.typ) | Typst | 95 | 0 | 1 | 96 | +| [经济学原理/hw/hw14.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw14.typ) | Typst | 41 | 0 | 2 | 43 | +| [经济学原理/hw/hw3.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw3.typ) | Typst | 51 | 0 | 1 | 52 | +| [经济学原理/hw/hw4.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw4.typ) | Typst | 46 | 0 | 4 | 50 | +| [经济学原理/hw/hw5.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw5.typ) | Typst | 18 | 0 | 0 | 18 | +| [经济学原理/hw/hw6.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw6.typ) | Typst | 122 | 0 | 4 | 126 | +| [经济学原理/hw/hw7.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw7.typ) | Typst | 24 | 8 | 0 | 32 | +| [经济学原理/hw/hw8.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw8.typ) | Typst | 51 | 0 | 0 | 51 | +| [经济学原理/hw/hw9.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw9.typ) | Typst | 49 | 0 | 0 | 49 | +| [经济学原理/微观部分.typ](/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/%E5%BE%AE%E8%A7%82%E9%83%A8%E5%88%86.typ) | Typst | 315 | 2 | 28 | 345 | +| [计算方法B/code/hw1/hw1.typ](/%E8%AE%A1%E7%AE%97%E6%96%B9%E6%B3%95B/code/hw1/hw1.typ) | Typst | 98 | 0 | 0 | 98 | +| [计算方法B/code/hw2/hw2.typ](/%E8%AE%A1%E7%AE%97%E6%96%B9%E6%B3%95B/code/hw2/hw2.typ) | Typst | 100 | 0 | 1 | 101 | +| [计算方法B/main.typ](/%E8%AE%A1%E7%AE%97%E6%96%B9%E6%B3%95B/main.typ) | Typst | 418 | 3 | 10 | 431 | +| [计算机网络/main.typ](/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/main.typ) | Typst | 13 | 2 | 1 | 16 | +| [计算机网络/数据链路层.typ](/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E6%95%B0%E6%8D%AE%E9%93%BE%E8%B7%AF%E5%B1%82.typ) | Typst | 284 | 0 | 3 | 287 | +| [计算机网络/第一节.typ](/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E7%AC%AC%E4%B8%80%E8%8A%82.typ) | Typst | 679 | 0 | 57 | 736 | +| [计算机网络/第一节_o.typ](/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E7%AC%AC%E4%B8%80%E8%8A%82_o.typ) | Typst | 571 | 0 | 46 | 617 | +| [计算机网络/网络层.typ](/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E7%BD%91%E7%BB%9C%E5%B1%82.typ) | Typst | 289 | 0 | 21 | 310 | +| [软件分析/hw/2100012990-郭子荀-软分第一次作业.typ](/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%B8%80%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ) | Typst | 16 | 0 | 0 | 16 | +| [软件分析/hw/2100012990-郭子荀-软分第三次作业.typ](/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%B8%89%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ) | Typst | 191 | 0 | 28 | 219 | +| [软件分析/hw/2100012990-郭子荀-软分第二次作业.typ](/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%BA%8C%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ) | Typst | 42 | 0 | 0 | 42 | +| [软件分析/hw/2100012990-郭子荀-软分第五次作业.typ](/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%BA%94%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ) | Typst | 61 | 15 | 2 | 78 | +| [软件分析/hw/2100012990-郭子荀-软分第四次作业.typ](/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E5%9B%9B%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ) | Typst | 43 | 0 | 0 | 43 | +| [软件分析/main.typ](/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/main.typ) | Typst | 424 | 0 | 13 | 437 | + +[Summary](results.md) / Details / [Diff Summary](diff.md) / [Diff Details](diff-details.md) \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/diff-details.md b/.VSCodeCounter/2024-10-17_10-15-14/diff-details.md new file mode 100644 index 0000000..59b2986 --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/diff-details.md @@ -0,0 +1,15 @@ +# Diff Details + +Date : 2024-10-17 10:15:14 + +Directory /home/yhtq/学习/课程 + +Total : 0 files, 0 codes, 0 comments, 0 blanks, all 0 lines + +[Summary](results.md) / [Details](details.md) / [Diff Summary](diff.md) / Diff Details + +## Files +| filename | language | code | comment | blank | total | +| :--- | :--- | ---: | ---: | ---: | ---: | + +[Summary](results.md) / [Details](details.md) / [Diff Summary](diff.md) / Diff Details \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/diff.csv b/.VSCodeCounter/2024-10-17_10-15-14/diff.csv new file mode 100644 index 0000000..b7d8d75 --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/diff.csv @@ -0,0 +1,2 @@ +"filename", "language", "", "comment", "blank", "total" +"Total", "-", , 0, 0, 0 \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/diff.md b/.VSCodeCounter/2024-10-17_10-15-14/diff.md new file mode 100644 index 0000000..d539fe9 --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/diff.md @@ -0,0 +1,19 @@ +# Diff Summary + +Date : 2024-10-17 10:15:14 + +Directory /home/yhtq/学习/课程 + +Total : 0 files, 0 codes, 0 comments, 0 blanks, all 0 lines + +[Summary](results.md) / [Details](details.md) / Diff Summary / [Diff Details](diff-details.md) + +## Languages +| language | files | code | comment | blank | total | +| :--- | ---: | ---: | ---: | ---: | ---: | + +## Directories +| path | files | code | comment | blank | total | +| :--- | ---: | ---: | ---: | ---: | ---: | + +[Summary](results.md) / [Details](details.md) / Diff Summary / [Diff Details](diff-details.md) \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/diff.txt b/.VSCodeCounter/2024-10-17_10-15-14/diff.txt new file mode 100644 index 0000000..061913c --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/diff.txt @@ -0,0 +1,22 @@ +Date : 2024-10-17 10:15:14 +Directory : /home/yhtq/学习/课程 +Total : 0 files, 0 codes, 0 comments, 0 blanks, all 0 lines + +Languages ++----------+------------+------------+------------+------------+------------+ +| language | files | code | comment | blank | total | ++----------+------------+------------+------------+------------+------------+ ++----------+------------+------------+------------+------------+------------+ + +Directories ++------+------------+------------+------------+------------+------------+ +| path | files | code | comment | blank | total | ++------+------------+------------+------------+------------+------------+ ++------+------------+------------+------------+------------+------------+ + +Files ++----------+----------+------------+------------+------------+------------+ +| filename | language | code | comment | blank | total | ++----------+----------+------------+------------+------------+------------+ +| Total | | 0 | 0 | 0 | 0 | ++----------+----------+------------+------------+------------+------------+ \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/results.csv b/.VSCodeCounter/2024-10-17_10-15-14/results.csv new file mode 100644 index 0000000..3003b8f --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/results.csv @@ -0,0 +1,106 @@ +"filename", "language", "Typst", "comment", "blank", "total" +"/home/yhtq/学习/课程/template.typ", "Typst", 403, 122, 31, 556 +"/home/yhtq/学习/课程/typst-sympy-calculator.typ", "Typst", 69, 3, 11, 83 +"/home/yhtq/学习/课程/代数学二/main.typ", "Typst", 10, 2, 0, 12 +"/home/yhtq/学习/课程/代数学二/习题课.typ", "Typst", 384, 2, 2, 388 +"/home/yhtq/学习/课程/代数学二/作业/hw1.typ", "Typst", 215, 2, 4, 221 +"/home/yhtq/学习/课程/代数学二/作业/hw10.typ", "Typst", 172, 0, 8, 180 +"/home/yhtq/学习/课程/代数学二/作业/hw11.typ", "Typst", 97, 0, 5, 102 +"/home/yhtq/学习/课程/代数学二/作业/hw12.typ", "Typst", 218, 0, 4, 222 +"/home/yhtq/学习/课程/代数学二/作业/hw2.typ", "Typst", 259, 2, 4, 265 +"/home/yhtq/学习/课程/代数学二/作业/hw3.typ", "Typst", 335, 23, 7, 365 +"/home/yhtq/学习/课程/代数学二/作业/hw4.typ", "Typst", 253, 15, 13, 281 +"/home/yhtq/学习/课程/代数学二/作业/hw5.typ", "Typst", 291, 11, 6, 308 +"/home/yhtq/学习/课程/代数学二/作业/hw6.typ", "Typst", 480, 0, 8, 488 +"/home/yhtq/学习/课程/代数学二/作业/hw7.typ", "Typst", 119, 0, 6, 125 +"/home/yhtq/学习/课程/代数学二/作业/hw8.typ", "Typst", 331, 1, 5, 337 +"/home/yhtq/学习/课程/代数学二/作业/hw9.typ", "Typst", 255, 0, 12, 267 +"/home/yhtq/学习/课程/代数学二/章节/test.typ", "Typst", 0, 0, 1, 1 +"/home/yhtq/学习/课程/代数学二/章节/上半学期.typ", "Typst", 3111, 11, 74, 3196 +"/home/yhtq/学习/课程/代数学二/章节/下半学期.typ", "Typst", 2455, 2, 45, 2502 +"/home/yhtq/学习/课程/几何学/main.typ", "Typst", 2646, 10, 123, 2779 +"/home/yhtq/学习/课程/复变函数/main.typ", "Typst", 2358, 4, 46, 2408 +"/home/yhtq/学习/课程/复变函数/作业/hw1.typ", "Typst", 102, 2, 8, 112 +"/home/yhtq/学习/课程/复变函数/作业/hw10.typ", "Typst", 65, 2, 0, 67 +"/home/yhtq/学习/课程/复变函数/作业/hw2.typ", "Typst", 120, 2, 3, 125 +"/home/yhtq/学习/课程/复变函数/作业/hw3.typ", "Typst", 87, 2, 1, 90 +"/home/yhtq/学习/课程/复变函数/作业/hw4.typ", "Typst", 108, 2, 1, 111 +"/home/yhtq/学习/课程/复变函数/作业/hw5.typ", "Typst", 56, 2, 2, 60 +"/home/yhtq/学习/课程/复变函数/作业/hw6.typ", "Typst", 46, 2, 0, 48 +"/home/yhtq/学习/课程/复变函数/作业/hw7.typ", "Typst", 91, 2, 0, 93 +"/home/yhtq/学习/课程/复变函数/作业/hw8.typ", "Typst", 321, 2, 6, 329 +"/home/yhtq/学习/课程/复变函数/作业/hw9.typ", "Typst", 81, 2, 1, 84 +"/home/yhtq/学习/课程/常微分方程/main.typ", "Typst", 2911, 8, 37, 2956 +"/home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 3.typ", "Typst", 341, 9, 4, 354 +"/home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 4.typ", "Typst", 194, 2, 2, 198 +"/home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 5.typ", "Typst", 135, 2, 2, 139 +"/home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 6.typ", "Typst", 132, 2, 3, 137 +"/home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 7.typ", "Typst", 340, 2, 6, 348 +"/home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 8.typ", "Typst", 256, 2, 5, 263 +"/home/yhtq/学习/课程/常微分方程/作业/hw1.typ", "Typst", 345, 8, 5, 358 +"/home/yhtq/学习/课程/常微分方程/作业/hw2.typ", "Typst", 568, 7, 7, 582 +"/home/yhtq/学习/课程/并行与分布式计算/main.typ", "Typst", 140, 0, 3, 143 +"/home/yhtq/学习/课程/抽象代数/main.typ", "Typst", 13, 6, 2, 21 +"/home/yhtq/学习/课程/抽象代数/作业/hw10.typ", "Typst", 719, 36, 12, 767 +"/home/yhtq/学习/课程/抽象代数/作业/hw11.typ", "Typst", 228, 12, 3, 243 +"/home/yhtq/学习/课程/抽象代数/作业/hw12.typ", "Typst", 324, 2, 5, 331 +"/home/yhtq/学习/课程/抽象代数/作业/hw2.typ", "Typst", 111, 2, 3, 116 +"/home/yhtq/学习/课程/抽象代数/作业/hw3.typ", "Typst", 598, 37, 73, 708 +"/home/yhtq/学习/课程/抽象代数/作业/hw4.typ", "Typst", 237, 2, 6, 245 +"/home/yhtq/学习/课程/抽象代数/作业/hw5.typ", "Typst", 344, 28, 6, 378 +"/home/yhtq/学习/课程/抽象代数/作业/hw6.typ", "Typst", 194, 2, 27, 223 +"/home/yhtq/学习/课程/抽象代数/作业/hw7.typ", "Typst", 654, 99, 22, 775 +"/home/yhtq/学习/课程/抽象代数/作业/hw8.typ", "Typst", 460, 30, 10, 500 +"/home/yhtq/学习/课程/抽象代数/作业/hw9.typ", "Typst", 232, 2, 13, 247 +"/home/yhtq/学习/课程/抽象代数/章节/模、域.typ", "Typst", 1414, 0, 15, 1429 +"/home/yhtq/学习/课程/抽象代数/章节/环.typ", "Typst", 795, 0, 29, 824 +"/home/yhtq/学习/课程/抽象代数/章节/群论.typ", "Typst", 1186, 0, 238, 1424 +"/home/yhtq/学习/课程/数学模型/main.typ", "Typst", 2443, 3, 50, 2496 +"/home/yhtq/学习/课程/数学模型/作业/hw2.typ", "Typst", 328, 9, 5, 342 +"/home/yhtq/学习/课程/数学模型/作业/hw3.typ", "Typst", 158, 2, 4, 164 +"/home/yhtq/学习/课程/数学模型/作业/hw4.typ", "Typst", 37, 2, 0, 39 +"/home/yhtq/学习/课程/数学模型/作业/hw5.typ", "Typst", 139, 9, 3, 151 +"/home/yhtq/学习/课程/数学模型/作业/hw6.typ", "Typst", 109, 6, 4, 119 +"/home/yhtq/学习/课程/数学模型/作业/hw7.typ", "Typst", 166, 2, 3, 171 +"/home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/changelog.typ", "Typst", 80, 0, 35, 115 +"/home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/contributors.typ", "Typst", 4, 0, 2, 6 +"/home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/template.typ", "Typst", 663, 107, 77, 847 +"/home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/thesis.typ", "Typst", 923, 5, 30, 958 +"/home/yhtq/学习/课程/数理逻辑/main.typ", "Typst", 484, 0, 10, 494 +"/home/yhtq/学习/课程/数理逻辑/作业/ml-1_1-hw.typ", "Typst", 141, 0, 6, 147 +"/home/yhtq/学习/课程/数理逻辑/作业/ml-1_2-hw.typ", "Typst", 165, 0, 3, 168 +"/home/yhtq/学习/课程/数理逻辑/作业/ml-2_1-hw.typ", "Typst", 214, 1, 8, 223 +"/home/yhtq/学习/课程/数理逻辑/作业/ml-2_2-hw.typ", "Typst", 112, 0, 0, 112 +"/home/yhtq/学习/课程/数理逻辑/作业/ml-3_1-hw.typ", "Typst", 81, 0, 2, 83 +"/home/yhtq/学习/课程/机器学习数学导引/main.typ", "Typst", 286, 0, 8, 294 +"/home/yhtq/学习/课程/机器学习数学导引/作业/hw1.typ", "Typst", 84, 0, 6, 90 +"/home/yhtq/学习/课程/机器学习数学导引/作业/hw2.typ", "Typst", 241, 0, 3, 244 +"/home/yhtq/学习/课程/机器学习数学导引/作业/hw3.typ", "Typst", 120, 0, 5, 125 +"/home/yhtq/学习/课程/经济学原理/hw/hw10.typ", "Typst", 104, 0, 0, 104 +"/home/yhtq/学习/课程/经济学原理/hw/hw11.typ", "Typst", 150, 0, 1, 151 +"/home/yhtq/学习/课程/经济学原理/hw/hw12.typ", "Typst", 83, 0, 1, 84 +"/home/yhtq/学习/课程/经济学原理/hw/hw13.typ", "Typst", 95, 0, 1, 96 +"/home/yhtq/学习/课程/经济学原理/hw/hw14.typ", "Typst", 41, 0, 2, 43 +"/home/yhtq/学习/课程/经济学原理/hw/hw3.typ", "Typst", 51, 0, 1, 52 +"/home/yhtq/学习/课程/经济学原理/hw/hw4.typ", "Typst", 46, 0, 4, 50 +"/home/yhtq/学习/课程/经济学原理/hw/hw5.typ", "Typst", 18, 0, 0, 18 +"/home/yhtq/学习/课程/经济学原理/hw/hw6.typ", "Typst", 122, 0, 4, 126 +"/home/yhtq/学习/课程/经济学原理/hw/hw7.typ", "Typst", 24, 8, 0, 32 +"/home/yhtq/学习/课程/经济学原理/hw/hw8.typ", "Typst", 51, 0, 0, 51 +"/home/yhtq/学习/课程/经济学原理/hw/hw9.typ", "Typst", 49, 0, 0, 49 +"/home/yhtq/学习/课程/经济学原理/微观部分.typ", "Typst", 315, 2, 28, 345 +"/home/yhtq/学习/课程/计算方法B/code/hw1/hw1.typ", "Typst", 98, 0, 0, 98 +"/home/yhtq/学习/课程/计算方法B/code/hw2/hw2.typ", "Typst", 100, 0, 1, 101 +"/home/yhtq/学习/课程/计算方法B/main.typ", "Typst", 418, 3, 10, 431 +"/home/yhtq/学习/课程/计算机网络/main.typ", "Typst", 13, 2, 1, 16 +"/home/yhtq/学习/课程/计算机网络/数据链路层.typ", "Typst", 284, 0, 3, 287 +"/home/yhtq/学习/课程/计算机网络/第一节.typ", "Typst", 679, 0, 57, 736 +"/home/yhtq/学习/课程/计算机网络/第一节_o.typ", "Typst", 571, 0, 46, 617 +"/home/yhtq/学习/课程/计算机网络/网络层.typ", "Typst", 289, 0, 21, 310 +"/home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第一次作业.typ", "Typst", 16, 0, 0, 16 +"/home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第三次作业.typ", "Typst", 191, 0, 28, 219 +"/home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第二次作业.typ", "Typst", 42, 0, 0, 42 +"/home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第五次作业.typ", "Typst", 61, 15, 2, 78 +"/home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第四次作业.typ", "Typst", 43, 0, 0, 43 +"/home/yhtq/学习/课程/软件分析/main.typ", "Typst", 424, 0, 13, 437 +"Total", "-", 39765, 706, 1463, 41934 \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/results.json b/.VSCodeCounter/2024-10-17_10-15-14/results.json new file mode 100644 index 0000000..b52a75f --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/results.json @@ -0,0 +1 @@ +{"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B9%B6%E8%A1%8C%E4%B8%8E%E5%88%86%E5%B8%83%E5%BC%8F%E8%AE%A1%E7%AE%97/main.typ":{"language":"Typst","code":140,"comment":0,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-2_1-hw.typ":{"language":"Typst","code":214,"comment":1,"blank":8},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-1_1-hw.typ":{"language":"Typst","code":141,"comment":0,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-1_2-hw.typ":{"language":"Typst","code":165,"comment":0,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-3_1-hw.typ":{"language":"Typst","code":81,"comment":0,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/main.typ":{"language":"Typst","code":484,"comment":0,"blank":10},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E7%AB%A0%E8%8A%82/test.typ":{"language":"Typst","code":0,"comment":0,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%B9%A0%E9%A2%98%E8%AF%BE.typ":{"language":"Typst","code":384,"comment":2,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/main.typ":{"language":"Typst","code":10,"comment":2,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E7%AB%A0%E8%8A%82/%E4%B8%8A%E5%8D%8A%E5%AD%A6%E6%9C%9F.typ":{"language":"Typst","code":3111,"comment":11,"blank":74},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%96%B9%E6%B3%95B/code/hw2/hw2.typ":{"language":"Typst","code":100,"comment":0,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E7%AB%A0%E8%8A%82/%E4%B8%8B%E5%8D%8A%E5%AD%A6%E6%9C%9F.typ":{"language":"Typst","code":2455,"comment":2,"blank":45},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%96%B9%E6%B3%95B/code/hw1/hw1.typ":{"language":"Typst","code":98,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E7%90%86%E9%80%BB%E8%BE%91/%E4%BD%9C%E4%B8%9A/ml-2_2-hw.typ":{"language":"Typst","code":112,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E5%9B%9B%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ":{"language":"Typst","code":43,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%B8%80%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ":{"language":"Typst","code":16,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%96%B9%E6%B3%95B/main.typ":{"language":"Typst","code":418,"comment":3,"blank":10},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%B8%89%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ":{"language":"Typst","code":191,"comment":0,"blank":28},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%BA%8C%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ":{"language":"Typst","code":42,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/main.typ":{"language":"Typst","code":424,"comment":0,"blank":13},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/main.typ":{"language":"Typst","code":13,"comment":2,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E7%AC%AC%E4%B8%80%E8%8A%82_o.typ":{"language":"Typst","code":571,"comment":0,"blank":46},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E7%AC%AC%E4%B8%80%E8%8A%82.typ":{"language":"Typst","code":679,"comment":0,"blank":57},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%BD%AF%E4%BB%B6%E5%88%86%E6%9E%90/hw/2100012990-%E9%83%AD%E5%AD%90%E8%8D%80-%E8%BD%AF%E5%88%86%E7%AC%AC%E4%BA%94%E6%AC%A1%E4%BD%9C%E4%B8%9A.typ":{"language":"Typst","code":61,"comment":15,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw13.typ":{"language":"Typst","code":95,"comment":0,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E7%BD%91%E7%BB%9C%E5%B1%82.typ":{"language":"Typst","code":289,"comment":0,"blank":21},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BD%91%E7%BB%9C/%E6%95%B0%E6%8D%AE%E9%93%BE%E8%B7%AF%E5%B1%82.typ":{"language":"Typst","code":284,"comment":0,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw11.typ":{"language":"Typst","code":150,"comment":0,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw12.typ":{"language":"Typst","code":83,"comment":0,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/%E5%BE%AE%E8%A7%82%E9%83%A8%E5%88%86.typ":{"language":"Typst","code":315,"comment":2,"blank":28},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw7.typ":{"language":"Typst","code":24,"comment":8,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw3.typ":{"language":"Typst","code":51,"comment":0,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw5.typ":{"language":"Typst","code":18,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw9.typ":{"language":"Typst","code":49,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw10.typ":{"language":"Typst","code":104,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw8.typ":{"language":"Typst","code":51,"comment":0,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw4.typ":{"language":"Typst","code":46,"comment":0,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/changelog.typ":{"language":"Typst","code":80,"comment":0,"blank":35},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw6.typ":{"language":"Typst","code":122,"comment":0,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/contributors.typ":{"language":"Typst","code":4,"comment":0,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/thesis.typ":{"language":"Typst","code":923,"comment":5,"blank":30},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E7%BB%8F%E6%B5%8E%E5%AD%A6%E5%8E%9F%E7%90%86/hw/hw14.typ":{"language":"Typst","code":41,"comment":0,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E8%AE%BA%E6%96%87/pkuthss-typst/template.typ":{"language":"Typst","code":663,"comment":107,"blank":77},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw7.typ":{"language":"Typst","code":166,"comment":2,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw3.typ":{"language":"Typst","code":158,"comment":2,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw5.typ":{"language":"Typst","code":139,"comment":9,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw4.typ":{"language":"Typst","code":37,"comment":2,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw2.typ":{"language":"Typst","code":328,"comment":9,"blank":5},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/%E4%BD%9C%E4%B8%9A/hw6.typ":{"language":"Typst","code":109,"comment":6,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw3.typ":{"language":"Typst","code":87,"comment":2,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw5.typ":{"language":"Typst","code":56,"comment":2,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw1.typ":{"language":"Typst","code":102,"comment":2,"blank":8},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%95%B0%E5%AD%A6%E6%A8%A1%E5%9E%8B/main.typ":{"language":"Typst","code":2443,"comment":3,"blank":50},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw9.typ":{"language":"Typst","code":81,"comment":2,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw2.typ":{"language":"Typst","code":120,"comment":2,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw4.typ":{"language":"Typst","code":108,"comment":2,"blank":1},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw7.typ":{"language":"Typst","code":91,"comment":2,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw10.typ":{"language":"Typst","code":65,"comment":2,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw6.typ":{"language":"Typst","code":46,"comment":2,"blank":0},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw8.typ":{"language":"Typst","code":321,"comment":2,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%A4%8D%E5%8F%98%E5%87%BD%E6%95%B0/main.typ":{"language":"Typst","code":2358,"comment":4,"blank":46},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E7%AB%A0%E8%8A%82/%E6%A8%A1%E3%80%81%E5%9F%9F.typ":{"language":"Typst","code":1414,"comment":0,"blank":15},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E7%AB%A0%E8%8A%82/%E7%BE%A4%E8%AE%BA.typ":{"language":"Typst","code":1186,"comment":0,"blank":238},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E7%AB%A0%E8%8A%82/%E7%8E%AF.typ":{"language":"Typst","code":795,"comment":0,"blank":29},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw11.typ":{"language":"Typst","code":228,"comment":12,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw9.typ":{"language":"Typst","code":232,"comment":2,"blank":13},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw3.typ":{"language":"Typst","code":598,"comment":37,"blank":73},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw7.typ":{"language":"Typst","code":654,"comment":99,"blank":22},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw10.typ":{"language":"Typst","code":719,"comment":36,"blank":12},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw5.typ":{"language":"Typst","code":344,"comment":28,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw4.typ":{"language":"Typst","code":237,"comment":2,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw8.typ":{"language":"Typst","code":460,"comment":30,"blank":10},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw6.typ":{"language":"Typst","code":194,"comment":2,"blank":27},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw2.typ":{"language":"Typst","code":111,"comment":2,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/template.typ":{"language":"Typst","code":403,"comment":122,"blank":31},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/typst-sympy-calculator.typ":{"language":"Typst","code":69,"comment":3,"blank":11},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/%E4%BD%9C%E4%B8%9A/hw2.typ":{"language":"Typst","code":241,"comment":0,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/%E4%BD%9C%E4%B8%9A/hw1.typ":{"language":"Typst","code":84,"comment":0,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/main.typ":{"language":"Typst","code":286,"comment":0,"blank":8},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw12.typ":{"language":"Typst","code":218,"comment":0,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%203.typ":{"language":"Typst","code":341,"comment":9,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%205.typ":{"language":"Typst","code":135,"comment":2,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%9C%BA%E5%99%A8%E5%AD%A6%E4%B9%A0%E6%95%B0%E5%AD%A6%E5%AF%BC%E5%BC%95/%E4%BD%9C%E4%B8%9A/hw3.typ":{"language":"Typst","code":120,"comment":0,"blank":5},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/hw1.typ":{"language":"Typst","code":345,"comment":8,"blank":5},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%207.typ":{"language":"Typst","code":340,"comment":2,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/hw2.typ":{"language":"Typst","code":568,"comment":7,"blank":7},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%208.typ":{"language":"Typst","code":256,"comment":2,"blank":5},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/main.typ":{"language":"Typst","code":2911,"comment":8,"blank":37},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%206.typ":{"language":"Typst","code":132,"comment":2,"blank":3},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw11.typ":{"language":"Typst","code":97,"comment":0,"blank":5},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw7.typ":{"language":"Typst","code":119,"comment":0,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%87%A0%E4%BD%95%E5%AD%A6/main.typ":{"language":"Typst","code":2646,"comment":10,"blank":123},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw3.typ":{"language":"Typst","code":335,"comment":23,"blank":7},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw9.typ":{"language":"Typst","code":255,"comment":0,"blank":12},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw5.typ":{"language":"Typst","code":291,"comment":11,"blank":6},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw1.typ":{"language":"Typst","code":215,"comment":2,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw10.typ":{"language":"Typst","code":172,"comment":0,"blank":8},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw4.typ":{"language":"Typst","code":253,"comment":15,"blank":13},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw8.typ":{"language":"Typst","code":331,"comment":1,"blank":5},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw2.typ":{"language":"Typst","code":259,"comment":2,"blank":4},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B/%E4%BD%9C%E4%B8%9A/2100012990%20%E9%83%AD%E5%AD%90%E8%8D%80%20%E5%B8%B8%E5%BE%AE%E5%88%86%E6%96%B9%E7%A8%8B%204.typ":{"language":"Typst","code":194,"comment":2,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/main.typ":{"language":"Typst","code":13,"comment":6,"blank":2},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E4%BB%A3%E6%95%B0%E5%AD%A6%E4%BA%8C/%E4%BD%9C%E4%B8%9A/hw6.typ":{"language":"Typst","code":480,"comment":0,"blank":8},"file:///home/yhtq/%E5%AD%A6%E4%B9%A0/%E8%AF%BE%E7%A8%8B/%E6%8A%BD%E8%B1%A1%E4%BB%A3%E6%95%B0/%E4%BD%9C%E4%B8%9A/hw12.typ":{"language":"Typst","code":324,"comment":2,"blank":5}} \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/results.md b/.VSCodeCounter/2024-10-17_10-15-14/results.md new file mode 100644 index 0000000..6991157 --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/results.md @@ -0,0 +1,61 @@ +# Summary + +Date : 2024-10-17 10:15:14 + +Directory /home/yhtq/学习/课程 + +Total : 104 files, 39765 codes, 706 comments, 1463 blanks, all 41934 lines + +Summary / [Details](details.md) / [Diff Summary](diff.md) / [Diff Details](diff-details.md) + +## Languages +| language | files | code | comment | blank | total | +| :--- | ---: | ---: | ---: | ---: | ---: | +| Typst | 104 | 39,765 | 706 | 1,463 | 41,934 | + +## Directories +| path | files | code | comment | blank | total | +| :--- | ---: | ---: | ---: | ---: | ---: | +| . | 104 | 39,765 | 706 | 1,463 | 41,934 | +| . (Files) | 2 | 472 | 125 | 42 | 639 | +| 代数学二 | 17 | 8,985 | 71 | 204 | 9,260 | +| 代数学二 (Files) | 2 | 394 | 4 | 2 | 400 | +| 代数学二/作业 | 12 | 3,025 | 54 | 82 | 3,161 | +| 代数学二/章节 | 3 | 5,566 | 13 | 120 | 5,699 | +| 几何学 | 1 | 2,646 | 10 | 123 | 2,779 | +| 复变函数 | 11 | 3,435 | 24 | 68 | 3,527 | +| 复变函数 (Files) | 1 | 2,358 | 4 | 46 | 2,408 | +| 复变函数/作业 | 10 | 1,077 | 20 | 22 | 1,119 | +| 常微分方程 | 9 | 5,222 | 42 | 71 | 5,335 | +| 常微分方程 (Files) | 1 | 2,911 | 8 | 37 | 2,956 | +| 常微分方程/作业 | 8 | 2,311 | 34 | 34 | 2,379 | +| 并行与分布式计算 | 1 | 140 | 0 | 3 | 143 | +| 抽象代数 | 15 | 7,509 | 258 | 464 | 8,231 | +| 抽象代数 (Files) | 1 | 13 | 6 | 2 | 21 | +| 抽象代数/作业 | 11 | 4,101 | 252 | 180 | 4,533 | +| 抽象代数/章节 | 3 | 3,395 | 0 | 282 | 3,677 | +| 数学模型 | 11 | 5,050 | 145 | 213 | 5,408 | +| 数学模型 (Files) | 1 | 2,443 | 3 | 50 | 2,496 | +| 数学模型/作业 | 6 | 937 | 30 | 19 | 986 | +| 数学模型/论文 | 4 | 1,670 | 112 | 144 | 1,926 | +| 数学模型/论文/pkuthss-typst | 4 | 1,670 | 112 | 144 | 1,926 | +| 数理逻辑 | 6 | 1,197 | 1 | 29 | 1,227 | +| 数理逻辑 (Files) | 1 | 484 | 0 | 10 | 494 | +| 数理逻辑/作业 | 5 | 713 | 1 | 19 | 733 | +| 机器学习数学导引 | 4 | 731 | 0 | 22 | 753 | +| 机器学习数学导引 (Files) | 1 | 286 | 0 | 8 | 294 | +| 机器学习数学导引/作业 | 3 | 445 | 0 | 14 | 459 | +| 经济学原理 | 13 | 1,149 | 10 | 42 | 1,201 | +| 经济学原理 (Files) | 1 | 315 | 2 | 28 | 345 | +| 经济学原理/hw | 12 | 834 | 8 | 14 | 856 | +| 计算方法B | 3 | 616 | 3 | 11 | 630 | +| 计算方法B (Files) | 1 | 418 | 3 | 10 | 431 | +| 计算方法B/code | 2 | 198 | 0 | 1 | 199 | +| 计算方法B/code/hw1 | 1 | 98 | 0 | 0 | 98 | +| 计算方法B/code/hw2 | 1 | 100 | 0 | 1 | 101 | +| 计算机网络 | 5 | 1,836 | 2 | 128 | 1,966 | +| 软件分析 | 6 | 777 | 15 | 43 | 835 | +| 软件分析 (Files) | 1 | 424 | 0 | 13 | 437 | +| 软件分析/hw | 5 | 353 | 15 | 30 | 398 | + +Summary / [Details](details.md) / [Diff Summary](diff.md) / [Diff Details](diff-details.md) \ No newline at end of file diff --git a/.VSCodeCounter/2024-10-17_10-15-14/results.txt b/.VSCodeCounter/2024-10-17_10-15-14/results.txt new file mode 100644 index 0000000..edecc0a --- /dev/null +++ b/.VSCodeCounter/2024-10-17_10-15-14/results.txt @@ -0,0 +1,168 @@ +Date : 2024-10-17 10:15:14 +Directory : /home/yhtq/学习/课程 +Total : 104 files, 39765 codes, 706 comments, 1463 blanks, all 41934 lines + +Languages ++----------+------------+------------+------------+------------+------------+ +| language | files | code | comment | blank | total | ++----------+------------+------------+------------+------------+------------+ +| Typst | 104 | 39,765 | 706 | 1,463 | 41,934 | ++----------+------------+------------+------------+------------+------------+ + +Directories ++---------------------------------------------------------+------------+------------+------------+------------+------------+ +| path | files | code | comment | blank | total | ++---------------------------------------------------------+------------+------------+------------+------------+------------+ +| . | 104 | 39,765 | 706 | 1,463 | 41,934 | +| . (Files) | 2 | 472 | 125 | 42 | 639 | +| 代数学二 | 17 | 8,985 | 71 | 204 | 9,260 | +| 代数学二 (Files) | 2 | 394 | 4 | 2 | 400 | +| 代数学二/作业 | 12 | 3,025 | 54 | 82 | 3,161 | +| 代数学二/章节 | 3 | 5,566 | 13 | 120 | 5,699 | +| 几何学 | 1 | 2,646 | 10 | 123 | 2,779 | +| 复变函数 | 11 | 3,435 | 24 | 68 | 3,527 | +| 复变函数 (Files) | 1 | 2,358 | 4 | 46 | 2,408 | +| 复变函数/作业 | 10 | 1,077 | 20 | 22 | 1,119 | +| 常微分方程 | 9 | 5,222 | 42 | 71 | 5,335 | +| 常微分方程 (Files) | 1 | 2,911 | 8 | 37 | 2,956 | +| 常微分方程/作业 | 8 | 2,311 | 34 | 34 | 2,379 | +| 并行与分布式计算 | 1 | 140 | 0 | 3 | 143 | +| 抽象代数 | 15 | 7,509 | 258 | 464 | 8,231 | +| 抽象代数 (Files) | 1 | 13 | 6 | 2 | 21 | +| 抽象代数/作业 | 11 | 4,101 | 252 | 180 | 4,533 | +| 抽象代数/章节 | 3 | 3,395 | 0 | 282 | 3,677 | +| 数学模型 | 11 | 5,050 | 145 | 213 | 5,408 | +| 数学模型 (Files) | 1 | 2,443 | 3 | 50 | 2,496 | +| 数学模型/作业 | 6 | 937 | 30 | 19 | 986 | +| 数学模型/论文 | 4 | 1,670 | 112 | 144 | 1,926 | +| 数学模型/论文/pkuthss-typst | 4 | 1,670 | 112 | 144 | 1,926 | +| 数理逻辑 | 6 | 1,197 | 1 | 29 | 1,227 | +| 数理逻辑 (Files) | 1 | 484 | 0 | 10 | 494 | +| 数理逻辑/作业 | 5 | 713 | 1 | 19 | 733 | +| 机器学习数学导引 | 4 | 731 | 0 | 22 | 753 | +| 机器学习数学导引 (Files) | 1 | 286 | 0 | 8 | 294 | +| 机器学习数学导引/作业 | 3 | 445 | 0 | 14 | 459 | +| 经济学原理 | 13 | 1,149 | 10 | 42 | 1,201 | +| 经济学原理 (Files) | 1 | 315 | 2 | 28 | 345 | +| 经济学原理/hw | 12 | 834 | 8 | 14 | 856 | +| 计算方法B | 3 | 616 | 3 | 11 | 630 | +| 计算方法B (Files) | 1 | 418 | 3 | 10 | 431 | +| 计算方法B/code | 2 | 198 | 0 | 1 | 199 | +| 计算方法B/code/hw1 | 1 | 98 | 0 | 0 | 98 | +| 计算方法B/code/hw2 | 1 | 100 | 0 | 1 | 101 | +| 计算机网络 | 5 | 1,836 | 2 | 128 | 1,966 | +| 软件分析 | 6 | 777 | 15 | 43 | 835 | +| 软件分析 (Files) | 1 | 424 | 0 | 13 | 437 | +| 软件分析/hw | 5 | 353 | 15 | 30 | 398 | ++---------------------------------------------------------+------------+------------+------------+------------+------------+ + +Files ++---------------------------------------------------------+----------+------------+------------+------------+------------+ +| filename | language | code | comment | blank | total | ++---------------------------------------------------------+----------+------------+------------+------------+------------+ +| /home/yhtq/学习/课程/template.typ | Typst | 403 | 122 | 31 | 556 | +| /home/yhtq/学习/课程/typst-sympy-calculator.typ | Typst | 69 | 3 | 11 | 83 | +| /home/yhtq/学习/课程/代数学二/main.typ | Typst | 10 | 2 | 0 | 12 | +| /home/yhtq/学习/课程/代数学二/习题课.typ | Typst | 384 | 2 | 2 | 388 | +| /home/yhtq/学习/课程/代数学二/作业/hw1.typ | Typst | 215 | 2 | 4 | 221 | +| /home/yhtq/学习/课程/代数学二/作业/hw10.typ | Typst | 172 | 0 | 8 | 180 | +| /home/yhtq/学习/课程/代数学二/作业/hw11.typ | Typst | 97 | 0 | 5 | 102 | +| /home/yhtq/学习/课程/代数学二/作业/hw12.typ | Typst | 218 | 0 | 4 | 222 | +| /home/yhtq/学习/课程/代数学二/作业/hw2.typ | Typst | 259 | 2 | 4 | 265 | +| /home/yhtq/学习/课程/代数学二/作业/hw3.typ | Typst | 335 | 23 | 7 | 365 | +| /home/yhtq/学习/课程/代数学二/作业/hw4.typ | Typst | 253 | 15 | 13 | 281 | +| /home/yhtq/学习/课程/代数学二/作业/hw5.typ | Typst | 291 | 11 | 6 | 308 | +| /home/yhtq/学习/课程/代数学二/作业/hw6.typ | Typst | 480 | 0 | 8 | 488 | +| /home/yhtq/学习/课程/代数学二/作业/hw7.typ | Typst | 119 | 0 | 6 | 125 | +| /home/yhtq/学习/课程/代数学二/作业/hw8.typ | Typst | 331 | 1 | 5 | 337 | +| /home/yhtq/学习/课程/代数学二/作业/hw9.typ | Typst | 255 | 0 | 12 | 267 | +| /home/yhtq/学习/课程/代数学二/章节/test.typ | Typst | 0 | 0 | 1 | 1 | +| /home/yhtq/学习/课程/代数学二/章节/上半学期.typ | Typst | 3,111 | 11 | 74 | 3,196 | +| /home/yhtq/学习/课程/代数学二/章节/下半学期.typ | Typst | 2,455 | 2 | 45 | 2,502 | +| /home/yhtq/学习/课程/几何学/main.typ | Typst | 2,646 | 10 | 123 | 2,779 | +| /home/yhtq/学习/课程/复变函数/main.typ | Typst | 2,358 | 4 | 46 | 2,408 | +| /home/yhtq/学习/课程/复变函数/作业/hw1.typ | Typst | 102 | 2 | 8 | 112 | +| /home/yhtq/学习/课程/复变函数/作业/hw10.typ | Typst | 65 | 2 | 0 | 67 | +| /home/yhtq/学习/课程/复变函数/作业/hw2.typ | Typst | 120 | 2 | 3 | 125 | +| /home/yhtq/学习/课程/复变函数/作业/hw3.typ | Typst | 87 | 2 | 1 | 90 | +| /home/yhtq/学习/课程/复变函数/作业/hw4.typ | Typst | 108 | 2 | 1 | 111 | +| /home/yhtq/学习/课程/复变函数/作业/hw5.typ | Typst | 56 | 2 | 2 | 60 | +| /home/yhtq/学习/课程/复变函数/作业/hw6.typ | Typst | 46 | 2 | 0 | 48 | +| /home/yhtq/学习/课程/复变函数/作业/hw7.typ | Typst | 91 | 2 | 0 | 93 | +| /home/yhtq/学习/课程/复变函数/作业/hw8.typ | Typst | 321 | 2 | 6 | 329 | +| /home/yhtq/学习/课程/复变函数/作业/hw9.typ | Typst | 81 | 2 | 1 | 84 | +| /home/yhtq/学习/课程/常微分方程/main.typ | Typst | 2,911 | 8 | 37 | 2,956 | +| /home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 3.typ | Typst | 341 | 9 | 4 | 354 | +| /home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 4.typ | Typst | 194 | 2 | 2 | 198 | +| /home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 5.typ | Typst | 135 | 2 | 2 | 139 | +| /home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 6.typ | Typst | 132 | 2 | 3 | 137 | +| /home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 7.typ | Typst | 340 | 2 | 6 | 348 | +| /home/yhtq/学习/课程/常微分方程/作业/2100012990 郭子荀 常微分方程 8.typ | Typst | 256 | 2 | 5 | 263 | +| /home/yhtq/学习/课程/常微分方程/作业/hw1.typ | Typst | 345 | 8 | 5 | 358 | +| /home/yhtq/学习/课程/常微分方程/作业/hw2.typ | Typst | 568 | 7 | 7 | 582 | +| /home/yhtq/学习/课程/并行与分布式计算/main.typ | Typst | 140 | 0 | 3 | 143 | +| /home/yhtq/学习/课程/抽象代数/main.typ | Typst | 13 | 6 | 2 | 21 | +| /home/yhtq/学习/课程/抽象代数/作业/hw10.typ | Typst | 719 | 36 | 12 | 767 | +| /home/yhtq/学习/课程/抽象代数/作业/hw11.typ | Typst | 228 | 12 | 3 | 243 | +| /home/yhtq/学习/课程/抽象代数/作业/hw12.typ | Typst | 324 | 2 | 5 | 331 | +| /home/yhtq/学习/课程/抽象代数/作业/hw2.typ | Typst | 111 | 2 | 3 | 116 | +| /home/yhtq/学习/课程/抽象代数/作业/hw3.typ | Typst | 598 | 37 | 73 | 708 | +| /home/yhtq/学习/课程/抽象代数/作业/hw4.typ | Typst | 237 | 2 | 6 | 245 | +| /home/yhtq/学习/课程/抽象代数/作业/hw5.typ | Typst | 344 | 28 | 6 | 378 | +| /home/yhtq/学习/课程/抽象代数/作业/hw6.typ | Typst | 194 | 2 | 27 | 223 | +| /home/yhtq/学习/课程/抽象代数/作业/hw7.typ | Typst | 654 | 99 | 22 | 775 | +| /home/yhtq/学习/课程/抽象代数/作业/hw8.typ | Typst | 460 | 30 | 10 | 500 | +| /home/yhtq/学习/课程/抽象代数/作业/hw9.typ | Typst | 232 | 2 | 13 | 247 | +| /home/yhtq/学习/课程/抽象代数/章节/模、域.typ | Typst | 1,414 | 0 | 15 | 1,429 | +| /home/yhtq/学习/课程/抽象代数/章节/环.typ | Typst | 795 | 0 | 29 | 824 | +| /home/yhtq/学习/课程/抽象代数/章节/群论.typ | Typst | 1,186 | 0 | 238 | 1,424 | +| /home/yhtq/学习/课程/数学模型/main.typ | Typst | 2,443 | 3 | 50 | 2,496 | +| /home/yhtq/学习/课程/数学模型/作业/hw2.typ | Typst | 328 | 9 | 5 | 342 | +| /home/yhtq/学习/课程/数学模型/作业/hw3.typ | Typst | 158 | 2 | 4 | 164 | +| /home/yhtq/学习/课程/数学模型/作业/hw4.typ | Typst | 37 | 2 | 0 | 39 | +| /home/yhtq/学习/课程/数学模型/作业/hw5.typ | Typst | 139 | 9 | 3 | 151 | +| /home/yhtq/学习/课程/数学模型/作业/hw6.typ | Typst | 109 | 6 | 4 | 119 | +| /home/yhtq/学习/课程/数学模型/作业/hw7.typ | Typst | 166 | 2 | 3 | 171 | +| /home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/changelog.typ | Typst | 80 | 0 | 35 | 115 | +| /home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/contributors.typ | Typst | 4 | 0 | 2 | 6 | +| /home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/template.typ | Typst | 663 | 107 | 77 | 847 | +| /home/yhtq/学习/课程/数学模型/论文/pkuthss-typst/thesis.typ | Typst | 923 | 5 | 30 | 958 | +| /home/yhtq/学习/课程/数理逻辑/main.typ | Typst | 484 | 0 | 10 | 494 | +| /home/yhtq/学习/课程/数理逻辑/作业/ml-1_1-hw.typ | Typst | 141 | 0 | 6 | 147 | +| /home/yhtq/学习/课程/数理逻辑/作业/ml-1_2-hw.typ | Typst | 165 | 0 | 3 | 168 | +| /home/yhtq/学习/课程/数理逻辑/作业/ml-2_1-hw.typ | Typst | 214 | 1 | 8 | 223 | +| /home/yhtq/学习/课程/数理逻辑/作业/ml-2_2-hw.typ | Typst | 112 | 0 | 0 | 112 | +| /home/yhtq/学习/课程/数理逻辑/作业/ml-3_1-hw.typ | Typst | 81 | 0 | 2 | 83 | +| /home/yhtq/学习/课程/机器学习数学导引/main.typ | Typst | 286 | 0 | 8 | 294 | +| /home/yhtq/学习/课程/机器学习数学导引/作业/hw1.typ | Typst | 84 | 0 | 6 | 90 | +| /home/yhtq/学习/课程/机器学习数学导引/作业/hw2.typ | Typst | 241 | 0 | 3 | 244 | +| /home/yhtq/学习/课程/机器学习数学导引/作业/hw3.typ | Typst | 120 | 0 | 5 | 125 | +| /home/yhtq/学习/课程/经济学原理/hw/hw10.typ | Typst | 104 | 0 | 0 | 104 | +| /home/yhtq/学习/课程/经济学原理/hw/hw11.typ | Typst | 150 | 0 | 1 | 151 | +| /home/yhtq/学习/课程/经济学原理/hw/hw12.typ | Typst | 83 | 0 | 1 | 84 | +| /home/yhtq/学习/课程/经济学原理/hw/hw13.typ | Typst | 95 | 0 | 1 | 96 | +| /home/yhtq/学习/课程/经济学原理/hw/hw14.typ | Typst | 41 | 0 | 2 | 43 | +| /home/yhtq/学习/课程/经济学原理/hw/hw3.typ | Typst | 51 | 0 | 1 | 52 | +| /home/yhtq/学习/课程/经济学原理/hw/hw4.typ | Typst | 46 | 0 | 4 | 50 | +| /home/yhtq/学习/课程/经济学原理/hw/hw5.typ | Typst | 18 | 0 | 0 | 18 | +| /home/yhtq/学习/课程/经济学原理/hw/hw6.typ | Typst | 122 | 0 | 4 | 126 | +| /home/yhtq/学习/课程/经济学原理/hw/hw7.typ | Typst | 24 | 8 | 0 | 32 | +| /home/yhtq/学习/课程/经济学原理/hw/hw8.typ | Typst | 51 | 0 | 0 | 51 | +| /home/yhtq/学习/课程/经济学原理/hw/hw9.typ | Typst | 49 | 0 | 0 | 49 | +| /home/yhtq/学习/课程/经济学原理/微观部分.typ | Typst | 315 | 2 | 28 | 345 | +| /home/yhtq/学习/课程/计算方法B/code/hw1/hw1.typ | Typst | 98 | 0 | 0 | 98 | +| /home/yhtq/学习/课程/计算方法B/code/hw2/hw2.typ | Typst | 100 | 0 | 1 | 101 | +| /home/yhtq/学习/课程/计算方法B/main.typ | Typst | 418 | 3 | 10 | 431 | +| /home/yhtq/学习/课程/计算机网络/main.typ | Typst | 13 | 2 | 1 | 16 | +| /home/yhtq/学习/课程/计算机网络/数据链路层.typ | Typst | 284 | 0 | 3 | 287 | +| /home/yhtq/学习/课程/计算机网络/第一节.typ | Typst | 679 | 0 | 57 | 736 | +| /home/yhtq/学习/课程/计算机网络/第一节_o.typ | Typst | 571 | 0 | 46 | 617 | +| /home/yhtq/学习/课程/计算机网络/网络层.typ | Typst | 289 | 0 | 21 | 310 | +| /home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第一次作业.typ | Typst | 16 | 0 | 0 | 16 | +| /home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第三次作业.typ | Typst | 191 | 0 | 28 | 219 | +| /home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第二次作业.typ | Typst | 42 | 0 | 0 | 42 | +| /home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第五次作业.typ | Typst | 61 | 15 | 2 | 78 | +| /home/yhtq/学习/课程/软件分析/hw/2100012990-郭子荀-软分第四次作业.typ | Typst | 43 | 0 | 0 | 43 | +| /home/yhtq/学习/课程/软件分析/main.typ | Typst | 424 | 0 | 13 | 437 | +| Total | | 39,765 | 706 | 1,463 | 41,934 | ++---------------------------------------------------------+----------+------------+------------+------------+------------+ \ No newline at end of file diff --git a/template.typ b/template.typ index 7578dbe..785971f 100644 --- a/template.typ +++ b/template.typ @@ -85,6 +85,7 @@ #let conjugateLeft(g, a) = $#g^(-1) #a #g$ #let conjugateRight(g, a) = $#g #a #g^(-1)$ #let quotient(G, H) = $#G\\#H$ +#let empty = "" #let lift = math.arrow.t #let quo = math.class("relation", $slash$) #let ord = math.op("ord") @@ -524,6 +525,7 @@ // Code block with line numbers show raw.where(block: true): it => { if not code_with_line_number { return it } + set text(font: ("Noto Serif CJK SC", "New Computer Modern Math")) let lines = it.text.split("\n") let length = lines.len() let i = 0 @@ -551,3 +553,4 @@ body } +#let prop = sym.prop \ No newline at end of file diff --git "a/\344\273\243\346\225\260\345\255\246\344\272\214/main.typ" "b/\344\273\243\346\225\260\345\255\246\344\272\214/main.typ" index 31ea039..62e36be 100644 --- "a/\344\273\243\346\225\260\345\255\246\344\272\214/main.typ" +++ "b/\344\273\243\346\225\260\345\255\246\344\272\214/main.typ" @@ -6,6 +6,7 @@ author: "YHTQ", date: none, logo: none, + withChapterNewPage: true ) #include "章节/上半学期.typ" -#include "章节/下半学期.typ" +#include "章节/下半学期.typ" \ No newline at end of file diff --git "a/\344\273\243\346\225\260\345\255\246\344\272\214/\347\253\240\350\212\202/\344\270\213\345\215\212\345\255\246\346\234\237.typ" "b/\344\273\243\346\225\260\345\255\246\344\272\214/\347\253\240\350\212\202/\344\270\213\345\215\212\345\255\246\346\234\237.typ" index aa039a2..f278922 100644 --- "a/\344\273\243\346\225\260\345\255\246\344\272\214/\347\253\240\350\212\202/\344\270\213\345\215\212\345\255\246\346\234\237.typ" +++ "b/\344\273\243\346\225\260\345\255\246\344\272\214/\347\253\240\350\212\202/\344\270\213\345\215\212\345\255\246\346\234\237.typ" @@ -396,7 +396,7 @@ #proof[ 注意到整闭是局部性质，由上面的定理不难推出该定理 ] - #pagebreak() + == 戴德金整环|Dedekind domains 这部分在数论课程中更加重要，本门课程不会要求太高 #definition[戴德金整环|Dedekind domains][ @@ -419,7 +419,7 @@ - 否则，$p sect ZZ$ 是极大理想，由 @integral-prime-containing 知 $p$ 也是极大理想 ] ] - #pagebreak() + == 分式理想 #definition[分式理想/可逆理想][ 设 $A$ 是整环，$K$ 是分式域： @@ -502,7 +502,7 @@ #proof[ 利用局部化，显然（注意到左推右需要利用诺特性和 @noether-fractional-ideal-finite，右推左需要利用分式理想都有限生成表明环是诺特的） ] - #pagebreak() + = Kahler-differentials 这部分是补充内容，讨论代数的导数和切空间等内容 #definition[derivation][ @@ -615,7 +615,7 @@ (F) quo (F^2) -> Omega_(B quo A) tensorProduct_B C -> Omega_(C quo A) -> 0 $ ] - #pagebreak() + = 完备化 == 拓扑阿贝尔群 #definition[拓扑阿贝尔群][ @@ -1103,7 +1103,7 @@ #corollary[][ 诺特环上有限个变元的形式幂级数环是诺特的 ] - #pagebreak() + = 维数理论 | Dimension theory == 维数 #definition[height, dimension][ @@ -1486,7 +1486,7 @@ #corollary[][ 设 $A$ 是 regular local ring ,$k = A quo m subset A$ ，则 $hat(A)$ 同构于 $k[[t_1, ..., t_d]]$ ] - #pagebreak() + = 同调代数 == 回顾 #definition[Abel 范畴][ diff --git "a/\345\271\266\350\241\214\344\270\216\345\210\206\345\270\203\345\274\217\350\256\241\347\256\227/main.typ" "b/\345\271\266\350\241\214\344\270\216\345\210\206\345\270\203\345\274\217\350\256\241\347\256\227/main.typ" index fd17ccd..ab75072 100644 --- "a/\345\271\266\350\241\214\344\270\216\345\210\206\345\270\203\345\274\217\350\256\241\347\256\227/main.typ" +++ "b/\345\271\266\350\241\214\344\270\216\345\210\206\345\270\203\345\274\217\350\256\241\347\256\227/main.typ" @@ -116,4 +116,27 @@ #definition[BSP 模型][ BSP (Bulk Synchronous Parallel) 模型是一种并行计算模型，其中有 $p$ 个处理器。计算过程分为多个超步，每个超步之内处理器单独计算，超步结束时处理器之间进行通信，同步所有状态。 ] += MPI（Message Passing Interface） + MPI 是一种消息传递接口，是一种标准。 + == 进程定位 + 在 MPI 中，每个进程处在一个通信域（communicator）中，每个通信域有一个唯一的标识符，可以通过这个标识符来定位进程。通信域中每个进程有一个标识符，称为 rank + == 阻塞/非阻塞通信 + == 点对点通信 + == 集合通信 + == 程序的并行性 + #definition[][ + 对于两个程序（进程）$P_1, P_2$，记 $I(P), O(P)$ 分别为 $P$ 程序需要读取/写入的数据集合 + ] + #theorem[Bernstein][ + 两个程序 $P_1, P_2$ 可以并行执行，记作 $P_1 || P_2$，如果 $O(P_1) sect I(P_2) = emptyset$ 且 $O(P_2) sect I(P_1) = emptyset$ 且 $O(P_1) sect O(P_2) = emptyset$ + ] + #definition[][ + 不满足 Bernstein 条件的程序会产生竞争条件和数据依赖，也就是两个进程同时访问了相同数据，且至少有一个进程写入了数据。这样的并行程序如果直接执行，其结果将不能确定。具体而言，数据依赖常常分为： + - 流依赖：read after write，RAW + - 反依赖：write after read，WAR + - 输出依赖：write after write，WAW + ] + #definition[][ + 当且仅当所有不可消除（有些数据依赖是可消除的，例如多个数求和即使产生输出依赖也不影响结果）的程序依赖得以满足后，并行程序满足串行一致性。 + ] diff --git "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" index 02e8129..c579ca3 100644 --- "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" +++ "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" @@ -5,6 +5,7 @@ author: "YHTQ", date: datetime.today().display(), logo: none, + withChapterNewPage: true ) #let not1 = math.tilde #let True = $T$ @@ -43,6 +44,7 @@ #let L2 = $"L2"$ #let L3 = $"L3"$ #let idL = $"引理" calA -> calA$ +#let language = $cal(L)$ = 前言 - 主要参考书：Introduction to Mathematical Logic - 成绩：平时 30%，期末 70% @@ -424,6 +426,69 @@ - 推理规则：MP ] 主流数学仍是基于经典逻辑的，但是其中有些分支也应用了直觉主义逻辑。 += 一阶逻辑：模型论 + == 谓词和量词 + 一阶逻辑就是在命题逻辑中将基本命题细分为： + - 谓词结构，形如 $A(x)$，表示对于任何变元（主词），谓词 $A$，产生基本命题 $A(x)$ + - 任意结构，形如 $forall x, A(x)$，表示对于任何 $x$，$A(x)$ 都成立 + - 存在结构，形如 $exists x, A(x)$，表示存在一个 $x$ 使得 $A(x)$ 成立 + #definition[][ + 被量词限定的变元称为自由变元，否则称为约束变元。含有自由变元的项往往无法确定真值。 + ] + == 一阶语言 + 本节给出一阶语言（记为 #language）的形式定义 + #definition[一阶语言的字符表][ + 一阶语言的字符表包括： + - 至多可数的变元集合 $x_1, x_2, ...$ + - 至多可数的常元集合 $a_1, a_2, ...$ + - 逻辑符号 $not1, infer$ + - 量词 $forall$ + - 谓词符 $A_m^n$，表示第 $m$ 个谓词符，有 $n$ 个参数 + - 函项符号 $f_m^n$，表示第 $m$ 个函项符号，有 $n$ 个参数 + ] + #remark[][ + 零元的谓词符/函项符事实上是常元/常命题，方便期间我们仍然保留额外定义的常元，但不额外定义常命题。 + ] + #definition[][ + 称 $language^+$ 为 $language$ 的一个扩展，如果它拓展了 $language$ 的变元集合/常元集合/谓词符/函项符 + ] + #definition[公式与项][ + 一阶语言中良好的表达式分为公式与项，满足文法规则： + ``` + term ::= x_i + | a_i + | f_m^n (term_1, ..., term_n) + formula ::= A_m^n (term_1, ..., term_n) + | not formula + | formula -> formula + | forall x_i, formula + ``` + 特别的： + - 只由常元和函项符构成的项称为闭项，否则称为开项。显然将一些闭项加入常元集可以得到拓展，称为闭项拓展。只用常元的拓展称为常元拓展。 + - 不含量词，变元的公式称为命题公式，也就是命题逻辑语言 $language_0$ 中的公式 + ] + #lemma[][ + #language 中的公式集和项集都是至多可数的 + ] + #definition[][ + 在公式 $forall x (calA)$ 中，称 $calA$ 是 $x$ 的辖域。$calA$ 中所有 $x$ 的出现以及 $forall x$ 中 $x$ 的出现称为约束的出现；变元在辖域之外的出现称为自由出现。 + ] + #example[][ + $forall x_1(A(x_1, x_2) -> forall x_2 (B(x_2)))$ 中，$x_1$ 约束出现两次，$x_2$ 约束出现一次，自由出现一次 + ] + #definition[替换][ + 设 $s, t$ 是项，将 $s$ 中所有 $x_i$ 替换为 $t$ 的操作记作 $s(x_i \/ t)$ + ] + #remark[][ + 替换是可能产生歧义的，例如： + $ + forall x_1 (x_2) + $ + 用 $x_1$ 替换 $x_2$ 会导致自由变元 $x_1$ 和约束变元 $x_1$ 产生混淆，这是非法的。 + ] + #definition[][ + 称 $t$ 在 $calA$ 中对 $x_i$ 是自由的，如果对于任意在 $t$ 中出现的变元 $x$， $calA$ 中所有形如 $forall x(calB)$ 的子公式均满足 $x_i$ 不在 $calB$ 中自由出现。 - + 如此，我们使用 $t$ 替换 $x_i$ 的所有自由出现便不会产生歧义。 + ] \ No newline at end of file diff --git "a/\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-2_2-hw.typ" "b/\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-2_2-hw.typ" new file mode 100644 index 0000000..f6198b6 --- /dev/null +++ "b/\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-2_2-hw.typ" @@ -0,0 +1,112 @@ +#import "../../template.typ": proof, note, corollary, lemma, theorem, definition, example, remark +#import "../../template.typ": * +#import "../main.typ": not1, True, False, infer +#import "../main.typ": * +#show: note.with( + title: "作业2_1", + author: "YHTQ", + date: datetime.today().display(), + logo: none, + withOutlined : false, + withTitle : false, + withHeadingNumbering: false +) +#set heading(numbering: + (..nums) => + { + let nums1 = nums.pos() + nums1.insert(0, 4) + numbering("1.1.(a)", ..nums1) + } +) += #empty + （本题中 $=$ 均指真值相等）\ + 由于替换原理，只需证明公理模式中变量均为元变量时情景即可。 + - $L1 : p_1 -> (p_2 -> p_1)$\ + 显然 $p_1 = True$ 时 $p_2 -> p_2 = True$，因此是重言式 + - $L2 : (p_1 -> (p_2 -> p_3)) -> ((p_1 -> p_2) -> (p_1 -> p_3))$\ + $p_1 = False$ 时公式化简为 $True -> (True -> True)$，$p_1 = True$ 时化简为 $(p_2 -> p_3) -> (p_2 -> p_3)$，都是重言式 + - $L3 : (not1 p_1 -> not1 p_2) -> (p_2 -> p_1) $\ + 注意到： + $ + (not1 p_1 -> not1 p_2) -> (p_2 -> p_1) &= (not1 not1 p_1 or not1 p_2) -> (not1 p_2 or p_1) \ + &= (p_1 or not1 p_2) -> (not1 p_2 or p_1) + $ + 而熟知 $p_1 or not1 p_2 = not1 p_2 or p_1$，因此上式是重言式 += #empty + == #empty + #let tL = $tack_L$ + #let tL1 = $tack_(L^+)$ + - 一方面，若 $calA$ 是 $L$ 中定理，则 $tL calB <=> {A} tack_L calB <=> tL1 calB$ + - 另一方面，假设 $calA$ 不是 $L$ 中定理，而它显然是 $L^+$ 中定理，因此定理集不同。 + == #empty + 由于 $L^+$ 只是比 $L$ 增加了公理，定理集扩大是显然的。\ + 在 $L$ 中有： + $ + (not1 p_1 -> p_2) -> (p_1 -> not1 p_2) = (not1 not1 p_1 or p_2) -> (not1 p_1 or not1 p_2) = (p_1 or p_2) -> (not1 p_1 or not1 p_2) + $ + 容易验证它不是永假式，因此 $not1 calA$ 不是重言式，由完全性定理它不是 $L$ 中定理，因此 $L$ 中加入 $not1 not1 calA$ 是一致扩张。熟知 $calA tack not1 not1 calA, not1 not1 calA tack calA$，因此这个扩张等价于 $L^+$，自然 $L^+$ 是一致的。 += #empty + 显然若 $calB$ 是矛盾，则 $calB models$ 任意公式，由完全性 $calB tL$ 所有公式，这将导致 $tL1$ 所有公式，意味着 $L^+$ 不是一致的。 += #empty + 由于 $J$ 是一致完全扩充，因此 $calA, not1 calA$ 恰有一个是其中定理： + - 如果 $calA$ 是定理，则加上 $calA$ 的扩张还是本身，当然是一致的 + - 如果 $calA$ 不是定理，则 $not1 calA$ 是定理，将导致扩充后 $calA, not1 calA$ 同时是定理，导致不一致性 += #empty + #let line = math.hyph.nobreak + #let lines(n) = $line$ * n + #let ax(x) = $#x line q #x p line$ + #let implyPre(x, y, z) = $#x q #y p #z $ + #let imply(x, y, z) = $#x line q #y p #z line$ + 取 $x = #lines(1)$，则 $ax(line)$ 是公理模式产生的公理\ + 取 $x = #lines(2), y = line, z = line$，则上面说明 $implyPre(#lines(2), line, line)$ 是定理，由推理规则 $imply(#lines(2), line, line)$ 是定理\ + #lemma[][ + 系统中定理一定形如 $x q y p z$，其中 $x, y, z$ 都只由 $line$ 构成 + ] + #proof[ + - 由公理模式生成的定理显然符合该形式 + - 由推理规则生成的定理显然也符合该形式 + 因此所有定理都符合该形式 + ] + 公式是否具有上述形式是容易判定的，不符合该形式的公式一定不是定理，因此下面只讨论符合该形式的公式。\ + #definition[][ + - 定义所有符合 @f-lemma 的公式集为 $cal(F)$，定理集为 $cal(T)$ + - 若 $x$ 是只由 #line 组成的公式，定义 $n(x)$ 为其中 #line 的数量，显然若 $x, y$ 都是这样的公式则 $x = y <=> n(x) = n(y)$ + - 定义： + $ + funcDef(v, cal(F), NN^3, x q y p z, (n(x), n(y), n(z))) + $ + @f-lemma 保证了定义合理，同时显然有 $v(x) = v(y) <=> x = y$ + ] + #lemma()[][ + 设 $calA in cal(F)$，则 $calA in cal(T) <=> v(calA) in v(cal(T))$ + ] + #proof[ + 前面已经说明 $v$ 是单射，做简单的集合逻辑运算即可。 + ] + #proposition[][ + - $calA$ 是公理模式生成的公理当且仅当 $exists n, v(calA) = (n+1, n, 1)$ + - 设 $calA$ 是定理且 $n(calA) = (r, s, t)$，则由推理规则生成的定理 $calB$ 满足 $(r+1, s, t+1)$ + - $v(cal(T)) + (1, 0, 1) subset v(cal(T))$ + ] + #proof[ + - 若 $calA$ 是公理模式生成的公理，则取 $n = n(x)$ 即可。反之，取 $x = n$ 个 #line 即可 + - 显然 + - 任取 $v(calA) in v(cal(T)) <=> calA in cal(T)$，则 $calA$ 利用推理规则生成的定理 $calB in cal(T)$ 恰好满足 $v(calB) = v(calA) + (1, 0, 1)$，因此 $v(calA) + (1, 0, 1) in v(cal(T))$，得证 + ] + #theorem[][ + 定义: + $ + funcDef(p, NN^3, NN^3, (a\, b\, c), (a+1\, b\, c+1))\ + funcDef(f, P(NN^3), P(NN^3), S, S union p(S))\ + $ + 并设 $S_0 = {(n+1, n, 1) | n in NN}$，则有： + $ + v(cal(T)) = union_(n in NN) f^n (S_0) + $ + 更进一步，它等于 $union_(n in NN) f^n ({(m + 1, m , 1) | m in NN}) = {(m + n + 1, m, n + 1) | m, n in NN}$ + ] + #proof[ + 由形式系统的定义及上面的命题，$v(cal(T))$ 就是 $S_0$ 在 $f$ 作用下的闭包，当然具有上面的形式。之后的计算是容易的。 + ] + @semantics 结合 @completeness 即可得到定理的判定方法。在 @semantics 给出的语义下，它是完全的，但并不完全是加法，因为从 @semantics 可以看出 $0 + 0$ 并不能在此语言中被表达。换言之，若以自然数加法为语义则它具有 soundness ，但不具有 completeness 。 \ No newline at end of file diff --git "a/\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-3_1-hw.typ" "b/\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-3_1-hw.typ" new file mode 100644 index 0000000..6a40fbe --- /dev/null +++ "b/\346\225\260\347\220\206\351\200\273\350\276\221/\344\275\234\344\270\232/ml-3_1-hw.typ" @@ -0,0 +1,83 @@ +#import "../../template.typ": proof, note, corollary, lemma, theorem, definition, example, remark +#import "../../template.typ": * +#import "../main.typ": not1, True, False, infer +#import "../main.typ": * +#show: note.with( + title: "作业2_1", + author: "YHTQ", + date: datetime.today().display(), + logo: none, + withOutlined : false, + withTitle : false, + withHeadingNumbering: false +) +#set heading(numbering: + (..nums) => + { + let nums1 = nums.pos() + nums1.insert(0, 5) + numbering("1.1.(a)", ..nums1) + } +) += #empty + == #empty + #let isFunc = $"is_func"$ + #let derivable = $"derivable"$ + #let continuous = $"continuous"$ + $not1 forall x (isFunc(x) -> derivable(x))$ + == #empty + $exists x (isFunc(x) and continuous(x) and not1 derivable(x))$ += #empty + 关关雎鸠，在河之洲。窈窕淑女，君子好逑。 + #let jj(x) = $"是雎鸠"(x)$ + #let gg(x) = $"正在关关和鸣"(x)$ + #let hz(x) = $"在河之洲"(x)$ + #let yt(x) = $"是窈窕淑女"(x)$ + #let jz(x) = $"是君子"(x)$ + #let hq(x, y) = $"好逑"(x, y)$ + $ + exists x(jj(x) and gg(x) and hz(x))\ + and forall x(yt(x) -> (forall y(jz(y) -> hq(x, y))))\ + $ += #empty + #let isCar = $"is_car"$ + #let hasFourWheels = $"has_four_wheels"$ + #let isHuman = $"is_human"$ + #let isLazy = $"is_lazy"$ + #let isSilly = $"is_silly"$ + == #empty + $ + not1 forall x(isCar(x) -> hasFourWheels(x))\ + $ + $ + exists x(isCar(x) and not1 hasFourWheels(x))\ + $ + == #empty + $ + not1 forall x(isHuman(x) -> not1 (isLazy(x) or isSilly(x)))\ + $ + $ + exists x(isHuman(x) and (isLazy(x) or isSilly(x)))\ + $ += #empty + == #empty + 这是项，不是公式 + == #empty + $A_1^3$ 是三元谓词符，此表达式中只有两个项作用在它上面，因此不是公式 += #empty + #let t1 = $f_1^2 (x_1, x_3)$ + == #empty + $x_1$ 自由出现一次，#t1 对 $x_2$ 自由，该公式中没有与 $x_1, x_3$ 相关的任意量词 + == #empty + $x_1$ 约束出现两次，#t1 对 $x_2$ 不自由，因为 $x_2$ 出现在了 $forall x_1$ 的辖域之中。 + += #empty + （条件保证了 $calA(x_i) -> calA(x_j)$ 的替换不会产生歧义，证明过程中并不会直接用到条件） + + 如若不然，假设 $calA(x_j)$ 中含有 $forall x_i (calB'(x_j))$ 其中 $x_j$ 在 $calB'(x_j)$ 中自由出现，按照替换的规则将有： + - 若其中含有由 $x_i$ 替换得到的 $x_j$，导致 $calA(x_i)$ 中含有 $forall x_i (calB'(x_i))$，但显然这样的 $x_i$ 不是自由出现的，因此不可能进行替换 + - 否则，其中 $x_j$ 都直接来自于 $calA(x_i)$，然而 $calA(x_i)$ 中 $x_j$ 都约束出现，换言之一定处在 $calA(x_i)$ 子公式： + - $forall x_j (calC (forall x_i (calB(x_j))))$ + 之中，而替换不改变 $x_j$，因此在 $calA(x_j)$ 中上两式形如： + - $forall x_j (calC' (forall x_i (calB'(x_j))))$ + 导致 $calB'(x_j)$ 中的 $x_j$ 一定都约束出现，与假设矛盾 \ No newline at end of file diff --git "a/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/main.typ" "b/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/main.typ" index a870f9c..e721f8b 100644 --- "a/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/main.typ" +++ "b/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/main.typ" @@ -5,6 +5,7 @@ author: "YHTQ", date: datetime.today().display(), logo: none, + withChapterNewPage: true ) = 前言 @@ -114,8 +115,179 @@ - Ridge Regression：$min_(beta) sum_(i=1)^n (y_i - beta^T x_i)^2 + lambda norm(beta)_2^2$ - Lasso Regression：$min_(beta) sum_(i=1)^n (y_i - beta^T x_i)^2 + lambda norm(beta)_1^2$，往往用于参数非常稀疏时 ] - #pagebreak() + == 分类问题 + 回归问题中，目标函数的值域是连续的实数域。而在分类问题中，值域只是离散的点。理论上讲，我们的损失函数尽可能多的准确拟合目标，但在实际上我们往往使用代替的损失函数，使得该损失函数降低时，确实意味着拟合更准确。 + + 分类问题可以从概率和几何两个角度进行考虑，分别可以产生两类不同的损失函数： + - 从概率角度，我们认为我们不是拟合函数，而是拟合一个值域上的概率分布。 + #definition[softmax][ + 对于一个 $d$ 维的输入 $x$，我们希望输出一个 $k$ 维的概率分布 $p$，其中 $p_i = P(y = i | x)$，这被称为 softmax 函数： + $ + p_i (x) = "softmax"(x)_i = (e^(x_i))/(sum_j e^(x^T beta_j)) + $ + ] + 由此，我们的优化目标变为： + $ + min_theta 1/n sum_(i=1)^n d(S(f_theta (x_i)), e_(y_i)) + $ + 其中 $d$ 用于度量两个概率分布的距离。 + #example[KL divergence][ + 通常我们使用 KL 散度来度量两个概率分布的距离： + $ + D(p, q) = sum_i p_i log(p_i/q_i) = -sum_i p_j log q_j - (-sum_i p_i log p_i) + $ + 或者连续情形： + $ + D(p, q) = integral_()^() p(x) log(p(x)/q(x)) dif x + $ + + 如果使用它作为 $d$，优化问题@classfication-target 恰好可以变形为： + $ + max_theta 1/n sum_(i = 1)^n log F_(y_i) (x_i \; theta) + $ + 这事实上就是一种极大似然估计。 + ] + #remark[Label Smoothing][ + 有些分类问题中，类别的差异本身就很小。此时，我们可以对 label 进行平滑，替代原有的 one hot 分布，也即将： + $ + (0, ..., 1,..., 0) -> (epsilon, ..., 1 - (n - 1) epsilon, epsilon) + $ + 之后再对@classfication-target 进行优化，可以让模型的输出更加平滑。 + ] + - 从几何角度，就是希望找到超平面将两种数据分离开。假设我们使用超平面： + $ + H = {x | beta^T x + beta_0 = 0} + $ + 并且假设 $norm(beta) = 1$。直觉上来说，我们希望点离超平面尽量远，因此可以设计优化问题： + $ + max (min_i abs(beta^T x_i + beta_0)) \ + s.t. space y_i(beta^T x_i + beta_0) >= 0 + $ + 这个形式并不方便求解。我们利用常见的技巧，将其化为等价的优化问题： + $ + max t with beta in S^(d-1), beta_0 in RR, t in RR, t >= 0\ + s.t. y_i (beta^T x_i + beta_0) >= t + $ + 进一步的： + $ + max t with beta in S^(d-1), beta_0 in RR, t in RR, t >= 0\ + s.t. y_i (beta^T/t x_i + beta_0/t) >= 1 + $ + 令 $beta = beta/t, beta_0 = beta_0/t$，得到： + $ + min norm(beta) with beta in RR^n, beta_0 in RR\ + s.t. y_i (beta^T x_i + beta_0) >= 1 + $ + 事实上，这就是在所有能够充分拟合数据的参数选择中，选取最简单的模型。这个思想可以推广到非线性中： + #algorithm[][ + 设 $cal(F)$ 是函数空间，$Omega: cal(F) -> RR^+$ 是复杂度，我们往往使用下面的模型： + $ + min Omega(f) s.t. f(x_i) y_i >= 1 + $ + 这里的 $f(x) y$ 往往称为 confidence 或者 margin。 + ] + 这里我们使用的是硬约束，可以设计软约束的版本，称作 Soft-SVM: + $ + min (norm(beta)^2 + 1/n sum_i xi_i) \ + s.t. y_i (beta^T x_i + beta_0) >= 1 - xi_i, \ + xi_i >= 0 + $ + 以及相应的一般化版本： + $ + min Omega(f) + 1/n sum_i xi_i\ + s.t. f(x_i) y_i >= 1 - xi_i, xi_i >= 0 + $ + 化简一下，事实上就是： + $ + min_f Omega(f) + 1/n sum_i max(0, 1 - y_i f(x_i)) + $ + 某种意义上，上式后者就是一个损失函数，而前者是一个正则化项。\ + 令： + $ + l(z) = max(0, 1 - z) + $ + 往往将其称为 Hinge loss，它相当于在预测比较 confidence 时损失为零，否则施加线性的惩罚。不难看出，它是常见的 $0-1$ loss 的一个上界。 + + 推广而言，我们可以调整损失函数获得其他算法。注意在分类问题中，决定结果的往往只是那些接近边缘的点。 + == 无监督学习 + 无监督学习往往包括以下问题： + - density estimation：估计数据的分布，往往由于维数灾难难以在高维空间中进行 + - dimension reduction：将高维数据映射到低维空间，同时尽可能保留结构 + - clustering：将数据分成若干类，类似于无监督的分类问题 + #let hrho = $hat(rho)$ + #algorithm[Histogram][ + 估计密度的一种简单方法是直方图法。将数据空间划分为若干个小区间，然后统计每个区间的数据点数目，用每个区间的数据点数目除以总数据点数目，就得到了密度的估计。这个方法比较通用，但不能很好的利用光滑性。 + ] + #algorithm[Kernel density estimation，KDE][ + 一种更加光滑的方法是核密度估计。设 $K$ 是一个核函数，定义： + $ + hrho(x) = 1/n sum_i K_h (x - x_i) + $ + 其中 $K$ 是一个光滑函数，且满足： + $ + K_h -> delta ("Kronecker") + $ + 并且： + - $K(x) >= 0$ + - $integral_()^() K(x) dif x = 1$ + - $K(x) = K(-x)$ + 常见的一维 $K(x)$ 包括： + - $K(x) = bold(1) (x)$，类似于 Histogram + - $K(x) = max (0, 1 - abs(x))$ + - $K(x) = 1/sqrt(2 pi) e^(- x^2 / 2) $ + 高维的核函数往往只是通过将一维的核函数乘积得到。这种核函数称为各向同性的。 + ] + #example[][ + 步长 $h$ 的选择往往是只能手工进行的。以高斯核为例，有： + $ + K_h (x) = 1/h^d sum_i K((x - x_i)/ h) + $ + 若 $h$ 取得很小，则模型会失去泛化能力。我们进行一些误差分析，假设 $x_i$ 独立同分布： + $ + E(hrho(x) - rho(x)) &= 1/n sum_i E(K_h (x - x_i)) - rho(x)\ + &= E(K_h (x - X)) - rho(x)\ + &= 1/h^d E(K((x - X)/h)) - rho(x)\ + &= 1/h^d E(K((x - X)/h)) - rho(x)\ + &= 1/h^d integral_()^() k(z) rho(x - z h) dif z - rho(x)\ + &= 1/h^d integral_()^() k(z) (rho(x - z h) - rho(x)) dif z \ + $ + 对 $rho$ 做泰勒展开，注意到 $k$ 的对称性，其一阶项直接消掉，因此有上式 $<= C_1 h^2$ 且 + $ + C_1 <= norm(nabla^2 rho) integral_()^() k(z) norm(z)^2 dif z + $ + 同时： + $ + E(hrho(x) - rho(x))^2 = E(hrho(x) - E hrho(x) + E hrho(x) - rho(x))^2 \ + = (E (hrho(x) - rho(x)))^2 + E (hrho(x) - E hrho(x))^2\ + "Var" (hrho(x)) <= 1/n E(K_h^2 (x - x_i))\ + = 1/n integral_()^() 1/(h^(2 d)) K^2 ((x - x')/h) rho(x') dif x'\ + <= 1/n 1/h^d integral_()^() K^2 (z) rho(x - z h) dif z\ + $ + ] + #algorithm[PCA][ + 主成分分析是常见的降维方法。假设我们的数据 $x_i$ 大约在一个 $k$ 维子空间中，也即存在 $k$ 个正交基 $v_i$，使得 $x_i approx sum_j beta_(i j) v_j$。也即化成下面的优化问题： + $ + min_(V, z_i, c) 1/n sum_i norm(x_i - V z_i - c)^2\ + $ + 其中 $V$ 是一个正交矩阵，同时可不妨设 $sum z_i = 0$，先固定 $V$，求导计算可得： + $ + c = 1/n sum_i x_i\ + V^T (x_i - V z_i - c) = 0 = V^T x_i - z_i -V^T c\ + z_i = V^T (x_i - c) + $ + 问题再化为： + $ + min 1/n sum_i norm(x_i - V V^T (x_i - c) - c)^2 + $ + 做中心化后： + $ + min 1/n sum_i norm(x_i - V V^T x_i)^2 = min 1/n norm(X = X W W^T) \ + = 1/n tr (X^T X) - tr (X^T X W W^T)\ + = 1/n tr (X^T X) - tr (W^T X^T X W) + $ + 而令 $tr (W^T X^T X W)$ 最大的 $W$ 就是 $X^T X$ 的前 $k$ 大的特征值对应的特征向量。 + ] + + = 现代机器学习（深度学习） - #pagebreak() = 理论基础 - #pagebreak() \ No newline at end of file diff --git "a/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/\344\275\234\344\270\232/hw3.typ" "b/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/\344\275\234\344\270\232/hw3.typ" new file mode 100644 index 0000000..666f30f --- /dev/null +++ "b/\346\234\272\345\231\250\345\255\246\344\271\240\346\225\260\345\255\246\345\257\274\345\274\225/\344\275\234\344\270\232/hw3.typ" @@ -0,0 +1,124 @@ +#import "../../template.typ": proof, note, corollary, lemma, theorem, definition, example, remark +#import "../../template.typ": * +#import "../main.typ": * +#show: note.with( + title: "作业3", + author: "YHTQ", + date: datetime.today().display(), + logo: none, + withOutlined : false, + withTitle : false, +) +#let index = $bold(1)$ + += #empty + 首先由熟知的不等式： + $ + max e^(z_j) <= ((sum_j (e^(z_j))^beta) / n)^(1 / beta) + $ + 取对数得： + $ + max z_j <= log((sum_j e^(beta z_j)) / n) / beta <= log(sum_j e^(beta z_j)) / beta + $ + 另一方面： + $ + log(sum_j e^(beta z_j)) / beta <= (log (n e^(beta max z_j))) / beta = max z_j + log n / beta + $ += #empty + == #empty + 显有若 $x_i$ 分类正确则 $p_i >= 1/C$，否则 $p_i < 1/2$. 假设 $x_i$ 分类错误，则有： + $ + 1/n sum_i -log p_i > 1/n (- log p_i) = 1/n (-log 1/2) = (log 2) / n + $ + 因此若 $cal(R) <= (log 2) / n$ 一定所有都分类正确 + == #empty + $ + sum_i index (y_i in.not argmax_j f_j (x_i)) <= sum_i -(log p_i)/(log 2) = 1/(log 2) cal(R) + $ + == #empty + #lemma[][ + 假设 $x_i > 0$ 严格递减，则有： + $ + 1 - x_0^lambda / (sum_i x_i^lambda) tilde (x_1/x_0)^lambda + $ + 这里 $tilde$ 是指 $lambda -> +infinity$ 时的等价无穷小 + ] + #proof[ + $(1 - x_0^lambda / (sum_i x_i^lambda)) / (x_1/x_0)^lambda = ((sum_(i > 0) x_i^lambda) / (sum_i x_i^lambda)) / (x_1/x_0)^lambda = (sum_(i > 0) (x_i / x_1)^lambda) x_0^lambda / (sum_i x_i^lambda) -> 1$ + ] + #lemma[][ + 设 $a, b > 0$ 是等价无穷小，则 $log(a), log(b)$ 是等价无穷大 + ] + #proof[ + $log(a) / log(b) = log(b dot a / b) / log(b) = 1 - log(a / b) / (log b) -> 1$ + ] + #lemma[][ + 假设对于每个 $i, x_(i j) > 0$ 关于 $j$ 严格递减，且 $x_(i 0)/x_(i 1)$ 也严格递减，则： + $ + (log (1/n sum_i - log (x_(i 0) / (sum_j x_(i j)))))/lambda -> log x_(0 1) - log x_(0 0) + $ + ] + #proof[ + 注意到有： + $ + -log (x_(i 0) / (sum_j x_(i j))) = -log (1 + x_(i 0) / (sum_j x_(i j)) - 1) tilde 1 - x_(i 0) / (sum_j x_(i j)) tilde (x_(i 1) / x_(i 0))^lambda\ + log (1/n sum_i - log (x_(i 0) / (sum_j x_(i j)))) tilde 1/n sum_i (x_(i 1) / x_(i 0))^lambda tilde 1/n (x_(0 1)/x_(0 0))^lambda + $ + 因此： + $ + (log (1/n sum_i - log (x_(i 0) / (sum_j x_(i j)))))/lambda tilde log(1/n (x_(0 1)/x_(0 0))^lambda )/lambda = log x_(0 1) - log x_(0 0) + $ + ] + 在上面的引理中代入 $e^(f_j (x_i))$ 并重新排序即得结论。 += #empty + == #empty + 记 $V_x^bot$ 为 ${x_i}$ 的正交补空间，对任意 $beta$ 可做正交分解： + $ + beta = beta_1 + beta_2, beta_2 in V_x^bot, beta_1 in V_x + $ + 则显然有： + $ + 1/n sum_i l(y_i f(x_i\; beta, beta_0)) + lambda/2 norm(beta)^2 = 1/n sum_i l(y_i f(x_i\; beta_1)) + lambda/2 norm(beta_1)^2 + lambda/2 norm(beta_2)^2 + $ + 显然对于最优解 $beta^*$ 应有 $beta_2 = 0$，也即 $beta^*$ 在 $V_x$ 上。代入 $beta^* = X alpha$，优化目标变为： + $ + 1/n sum_i l(y_i (alpha^T X^T x_i + beta_0)) + lambda/2 alpha^T X^T X alpha + $ + 对 $alpha$ 求导，得： + $ + 0 = 1/n sum_i y_i X^T x_i l'(y_i (alpha^T X^T x_i + beta_0)) + lambda X^T X alpha = 1/n sum_i y_i X^T x_i l'(gamma_i^star) + lambda X^T X alpha + $ + 显有 $abs(alpha_i) prop l'(gamma_i^star)$ + == #empty + === #empty + $ + l'(gamma_i^star) = - e^(-gamma_i^star) + $ + 显有 $abs(alpha_i) prop e^(-gamma_i^star)$ + === #empty + 当 $gamma_i^* > 1$ 时，不难发现有 $l' (gamma_i^star) = 0$，因此只能有 $alpha_i = 0$ + === #empty + $alpha_i$ 可以看作数据点 $x_i$ 的权重，当 $l' (gamma_i^star)$ 较大时，对应数据点对于分类结果非常敏感，说明该数据点对于分类结果的贡献较大，因此 $alpha_i$ 也应该较大。 += #empty + == #empty + 由约束条件，不难得到： + $ + epsilon_i >= max(0, 1 - y_i f(x_i)) + $ + 假设 $t$ 单调递增，则目标取最小值时，显有： + $ + epsilon_i = max(0, 1 - y_i f(x_i)) + $ + 原问题变成： + $ + min_(f in cal(F)) lambda Omega(f) + 1/n sum_i t(max(0, 1 - y_i f(x_i))) + $ + == #empty + 为使： + $ + t(max(0, 1 - y_i f(x_i))) = (max(0, 1 - y_i f(x_i)))^2 + $ + 显然取 $t(x) = x^2$ 即可。 + + + diff --git "a/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw2/hw2.typ" "b/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw2/hw2.typ" new file mode 100644 index 0000000..2e1565d --- /dev/null +++ "b/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw2/hw2.typ" @@ -0,0 +1,101 @@ +#import "../../../template.typ": * +#show: note.with( + title: "作业2", + author: "YHTQ", + date: datetime.today().display(), + logo: none, + withOutlined : false, + withTitle : false, + withHeadingNumbering: false +) += 2 + 注意到 $norm(x + y) = norm(x) + norm(y)$ 等价于柯西不等式： + $ + inner(x, y) <= norm(x) norm(y) + $ + 取等，显然当且仅当 $x, y$ 线性相关且 $inner(x, y) = x^T y >= 0$ += 3 + $ + norm(A)_F^2 = sum_(i j) a_(i j)^2 = sum_j (sum_i a_(i j)^2) = sum_j norm(a_i)^2_2 + $ += 4 + #let bc = autoRVecNF(i => $beta_#i$, $n$) + #let abc = autoRVecNF(i => $A beta_#i$, $n$) + #let nf(A) = $norm(#A)_f$ + #let nf2(A) = $norm(#A)_f^2$ + #let n2(A) = $norm(#A)_2$ + #let n22(A) = $norm(#A)_2^2$ + + 设 $B = bc$，则： + $ + nf2(A B) = nf2(abc) = sum_j n2(A beta_j) <= sum_j n22(A) n22(beta_j) = n22(A) sum_j n22(beta_j) \ + = n22(A) nf2(B) + $ + 开方即得 $nf(A B) <= n2(A) nf(B)$\ + 另一方面，有： + $ + nf(A B) = nf((A B)^T) = nf(B^T A^T) <= n2(B^T) nf(A^T) = n2(B) nf(A) + $ + 就是第二个不等式 += 8 + #let suma = sumf() + #let summ = sumf(lower: $m$) + 考虑形式幂级数： + $ + suma A^n + $ + 断言它收敛，事实上使用柯西准则： + $ + norm(summ A^n) <= summ norm(A^n) <= summ norm(A)^n -> 0 + $ + 因此一定收敛。设其和为 $B$，则： + $ + B (I - A) = (suma A^n)(I - A) = I + $ + 表明 $B$ 就是 $I-A$ 的逆，并且： + $ + norm(B) = norm(suma A^n) <= suma norm(A^n) <= suma norm(A)^n = 1/(1 - norm(A)) + $ + 证毕 += 11 + == 1. #empty + $ + A = mat(375, 374;752, 750)\ + mat(1, 0;-2, 1) A = mat(375, 374;2, 2)\ + mat(1, 0;-1, 1/2) A = mat(375, 374;1, 1)\ + mat(375, -187;-1, 1/2) A = mat(1, 0;1, 1)\ + mat(375, -187;-376, 187.5) A = mat(1, 0;0, 1)\ + $ + $kappa_infinity A = norm(A) norm(Inv(A)) = 1502 * 188.5 = #(1502 * 188.5) $ + == 2. + #let b1 = -376 + 187.5 * 375 / 187 + #let b1s = repr(-376 + 187.5 * 375 / 187) + 等式变为： + $ + x = Inv(A) b + $ + 取 $b = vec(1, 375/187)$，则： + $ + x = vec(0, b1s) + $ + 做微扰： + $ + Inv(A) (b + vec(epsilon_1, epsilon_2)) = vec(375 epsilon_1 - 187 epsilon_2, b1 - 376 epsilon_1 + 187.5 epsilon_2) + $ + $epsilon_1, epsilon_2$ 很小时，$b$ 变化量很小，但： + $ + norm(delta x)/norm(x) >= abs(375 epsilon_1 - 187 epsilon_2)/b1s = abs(#repr(375 / b1) epsilon_1 - #repr(187 / b1) epsilon_2) >= 1 + $ + == 3. #empty + #let c1 = 374 * 752 / 375 - 750 + #let c1s = repr(c1) + 取 $x = vec(374/375, -1)$，则： + $ + A x = vec(0, c1s)\ + A (x + vec(epsilon_1, epsilon_2)) = vec( 375 epsilon_1 + 374 epsilon_2, c1s + + 752 epsilon_1 + 750 epsilon_2) + $ + $epsilon_1, epsilon_2$ 很小时，$x$ 变化量很小，但： + $ + norm(delta b)/norm(b) >= abs(375 epsilon_1 + 374 epsilon_2)/(c1s) = abs(#repr(375 / c1) epsilon_1 + #repr(374 / c1) epsilon_2) + $ \ No newline at end of file diff --git "a/\350\256\241\347\256\227\346\226\271\346\263\225B/main.typ" "b/\350\256\241\347\256\227\346\226\271\346\263\225B/main.typ" index 6adde83..a780b22 100644 --- "a/\350\256\241\347\256\227\346\226\271\346\263\225B/main.typ" +++ "b/\350\256\241\347\256\227\346\226\271\346\263\225B/main.typ" @@ -295,4 +295,136 @@ #proof[ 使用 Jordan 分解即可。 ] + #corollary[][ + 假设 $norm(I) = 1, norm(A) < 1$，则 $I - A$ 可逆，且有： + $ + norm(Inv((I - A))) <= 1/(1 - norm(A)) + $ + ] + #proof[ + #let suma = sumf() + #let summ = sumf(lower: $m$) + 考虑形式幂级数： + $ + suma A^n + $ + 断言它收敛，事实上使用柯西准则： + $ + norm(summ A^n) <= summ norm(A^n) <= summ norm(A)^n -> 0 + $ + 因此一定收敛。设其和为 $B$，则： + $ + B (I - A) = (suma A^n)(I - A) = I + $ + 表明 $B$ 就是 $I-A$ 的逆，并且： + $ + norm(B) = norm(suma A^n) <= suma norm(A^n) <= suma norm(A)^n = 1/(1 - norm(A)) + $ + 证毕 + ] + == 线性方程组的敏度分析 + 本节中，我们希望计算解线性方程组的条件数。假设我们使用的范数满足 $norm(I) = 1$，对线性方程组问题： + $ + A x = b + $ + 其中 $A$ 非奇异，假设微扰后变为： + $ + (A + delta A)(x + delta x) = b + delta b\ + A x + A delta x + delta A x + delta A delta x = b + delta b\ + A delta x + delta A x + delta A delta x= delta b\ + (A +delta A)delta x = delta b - delta A x\ + delta x = Inv((A + delta A)) (delta b - delta A x) = Inv((I + Inv(A) delta A)) Inv(A) (delta b - delta A x)\ + norm(delta x) <= norm(Inv((I + Inv(A) delta A))) norm(Inv(A)) (norm(delta b) + norm(delta A) norm(x))\ + norm(delta x)/norm(x) <= norm(Inv((I + Inv(A) delta A))) norm(Inv(A)) (norm(delta b)/norm(x) + norm(delta A) )\ + norm(delta x)/norm(x) <= norm(Inv((I + Inv(A) delta A))) norm(Inv(A)) (norm(delta b)/norm(x) + norm(delta A) ) <= (norm(A) norm(Inv(A)) ) / (1 - norm(Inv(A)) norm(delta A)) (norm(delta b)/(norm(A) norm(x)) + norm(delta A)/norm(A) )\ + <= (norm(A) norm(Inv(A)) ) / (1 - norm(Inv(A)) norm(delta A)) (norm(delta b)/(norm(A x)) + norm(delta A)/norm(A) ) + <= (norm(A) norm(Inv(A)) ) / (1 - norm(Inv(A)) norm(delta A)) (norm(delta b)/(norm(b)) + norm(delta A)/norm(A) ) + $ + 其中运用了： + $ + norm(Inv((I + Inv(A) delta A))) <= 1/(1 - norm(Inv(A) delta A)) <= 1/(1 - norm(Inv(A)) norm(delta A)) + $ + 因此我们得到定理： + #theorem[][ + 假设 $A x =b$ 经微扰变为 $(A + delta A)(x + delta x) = b + delta b$，则有： + $ + (delta x) / x <= (norm(A) norm(Inv(A)) ) / (1 - norm(Inv(A)) norm(delta A)) (norm(delta b)/norm(b) + norm(delta A)/norm(A) ) + $ + 若令 $kappa(A) = norm(A) norm(Inv(A))$，则上式表明 $(delta x)/x$ 与 $kappa(A)$ 大约为线性，因此 $kappa(A)$ 称为线性方程组问题的条件数。 + ] + 此外，我们有： + #theorem[][ + 在求逆问题中，有： + $ + (norm((A + delta A)^(-1) - A^(-1))) / norm(A^(-1)) &<= norm(I - A (A + delta A)^(-1)) = norm(I - Inv((I + delta A Inv(A))))\ + &= norm(((I + delta A Inv(A)) - I)Inv((I + delta A Inv(A))))\ + &<= norm(delta A) norm(Inv(A)) norm(Inv((I + delta A Inv(A))))\ + &<= (norm(delta A) norm(Inv(A)))/(1 - norm(delta A) norm(Inv(A)))\ + &= (norm(A) norm(Inv(A)))/(1 - norm(delta A) norm(Inv(A))) norm(delta A)/norm(A)\ + $ + 可见 $kappa(A)$ 也是求逆问题的条件数。 + ] + #theorem[][ + 若使用谱范数，则有： + $ + min {norm(delta A) | A +delta A "奇异"} = 1/norm(Inv(A)) + $ + ] + #proof[ + 由于谱范数是算子范数，取 $x$ 使得： + $ + norm(Inv(A) x) = norm(Inv(A)) + $ + 取： + $ + y = (Inv(A) x)/norm(Inv(A) x)\ + $ + 则： + $ + A y = x/norm(x) = (x y^T y)/(norm(x)) = (x y^T)/norm(x) y + $ + 也即： + $ + (A - (x y^T)/norm(x)) y = 0 + $ + 同时： + $ + norm((x y^T)/norm(x)) = 1/norm(x) sqrt(norm(x y^T y x^T)) = sqrt(norm(x x^T))/norm(x) = sqrt(norm(x^T x))/norm(x) = 1 + $ + 表明 $A - (x y^T)/norm(x)$ 是奇异的，而 $(x y^T)/norm(x)$ 就是我们要找的微扰。 + + 对于更小的微扰，@norm-inv 保证矩阵一定可逆。 + ] += 线性最小二乘问题 + #definition[最小二乘][ + 给定 $A in RR^(m times n), b in RR^m$，线性最小二乘问题是求解： + $ + min norm(A x - b)^2 + $ + 其中 $x in RR^n$ 为未知向量。 + ] + 显然 + - 若 $m = n$ 且 $A$ 非奇异时，$x = Inv(A) b$ 即可 + - 若 $m < n$，称作嵌进方程组，解有无穷多组，我们往往希望解出： + $ + min norm(x)^2 s.t. A x = b + $ + 也即范数最小的解。对于这种问题，我们往往通过拉格朗日乘子法解决。 + - 若 $m > n$，称方程组超定 (overdetermined)，我们希望解出： + $ + min norm(A x - b)^2 + $ + 也即最小化误差的平方和。这种问题的解法是线性最小二乘问题。当我们采用2-范数时，这是凸问题，存在唯一的最优解，求导可得解就是以下线性方程组的解： + $ + A^T A x = A^T b + $ + 这被称为最小二乘问题的正则化方程，线性代数的知识保证了它总是有解的。假设 $A$ 列满秩，则 $A^T A$ 对称正定，使用平方根法即可，否则用一般的解线性方程组方法即可。 + 然而，注意到 $A^T A$ 的条件数是 $A$ 的条件数的平方，因此使用一般的线性方程组解法会导致误差放大，因此我们希望采用其他方法求解。之前高斯变换我们使用的是初等变换矩阵，这里我们改用初等正交矩阵： + #definition[][ + 对于任意向量 $v$，令： + $ + H = I - 2/ (v^T v) v v^T + $ + 这样的矩阵称为 Householder 矩阵，对应向量称为 Householder 向量 。它是对称的正交/对合矩阵，且 $v$ 是特征向量，对应特征值为 $-1$。事实上，它就是关于超平面 $v^T$ 的反射。 + ] diff --git "a/\350\275\257\344\273\266\345\210\206\346\236\220/hw/2100012990-\351\203\255\345\255\220\350\215\200-\350\275\257\345\210\206\347\254\254\344\272\224\346\254\241\344\275\234\344\270\232.typ" "b/\350\275\257\344\273\266\345\210\206\346\236\220/hw/2100012990-\351\203\255\345\255\220\350\215\200-\350\275\257\345\210\206\347\254\254\344\272\224\346\254\241\344\275\234\344\270\232.typ" new file mode 100644 index 0000000..1d71e89 --- /dev/null +++ "b/\350\275\257\344\273\266\345\210\206\346\236\220/hw/2100012990-\351\203\255\345\255\220\350\215\200-\350\275\257\345\210\206\347\254\254\344\272\224\346\254\241\344\275\234\344\270\232.typ" @@ -0,0 +1,77 @@ +#import "../../template.typ": proof, note, corollary, lemma, theorem, definition, example, remark +#import "../../template.typ": * +#show: note.with( + title: "作业5", + author: "YHTQ", + date: datetime.today().display(), + logo: none, + withOutlined : false, + withTitle : false, + withHeadingNumbering: false +) += #empty + #let Inv(f, ori, res) = $"Inv"(#f\;#ori\;#res)$ + #let bT = $bold("True")$ + #let bF = $bold("False")$ + #let T = $"True"$ + #let F = $"False"$ + 用 $[a, b]$ 表示一个整数区间，布尔值的抽象域为 ${bot, bT, bF, top}$ ，（真实值记为 $#T, #F$），$Inv(f, "ori", "res")$ 表示运算 $f$ 在参数初始状态为 ori ，运算结果为 res 时的反向语义。$\_$ 表示任意抽象值，规则按照从上到下匹配。 + == 逻辑与 + - $Inv(and, (\_, \_), bot) = (bot, bot)$ + - $Inv(and, (\_, \_), bT) = (bT, bT)$ + // - $Inv(and, (bT, x), bT) = (bT, x)$ + // - $Inv(and, (x, bT), bT) = (x, bT)$ + - $Inv(and, (bT, \_), bF) = (bT, bF)$ + - $Inv(and, (\_, bT), bF) = (bF, bT)$ + - $Inv(and, (bot, bot), bF "or" top) = (top, top)$ + - $Inv(and, (bot, x), bF "or" top) = (top, x)$ + - $Inv(and, (x, bot), bF "or" top) = (x, top)$ + - $Inv(and, (x, y), bF "or" top) = (x, y)$ + == 逻辑非 + - $Inv(not, \_, bot) = (bot, bot)$ + - $Inv(not, \_, bT) = (bF)$ + - $Inv(not, \_, bF) = (bT)$ + - $Inv(not, bot, top) = (top)$ + - $Inv(not, x, top) = (x)$ + == 大于 + - $Inv(>, ([\_, \_], [\_, \_]), bot) = ([-infinity, infinity], [-infinity, infinity])$ + - $Inv(>, ([a, b], [c, d]), bT) = ([max(a, c + 1), b], [c, min(b - 1, d)])$ + - $Inv(>, ([a, b], [c, d]), bF) = ([a, min(b, d)], [max(a, c), b])$ + - $Inv(>, ([a, b], [c, d]), top) = ([a, b], [c, d])$ + == 加法 + - $Inv(+, ([\_, \_], [\_, \_]), bot) = ([-infinity, infinity], [-infinity, infinity])$ + - $Inv(+, ([a, b], [c, d]), [e, f]) = ([max(a, e - d), min(b, f - c)], [max(c, e - b), min(d, f - a)])$ + 对于表达式： + $ + (x >= 0) and (x >= 1 + y) and (y >= 1 + x) = #T + $ + （假设对于三个表达式从右向左更新） + - 第一轮结束：$(x, y): ([0, +infinity], [-infinity, +infinity])$ + - 第二轮结束：$(x, y): ([2, +infinity], [1, +infinity])$ + - 第三轮结束：$(x, y): ([4, +infinity], [3, +infinity])$ + - ...... + 迭代过程将无法终止。不过，上面的反向语义是单调的，同时若假设表达式是可满足的，则半格的高度将有限。具体而言，布尔值的半格当然是有限的，而对于任意变量 $X$，假设 $x$ 是一个可以使表达式成立的真实值，在算法的运行过程中，要么 $X$ 的下界为 $-infinity$，要么在某一轮被更新为某个值 $X_m$，由单调性，算法过程中下界将不会小于 $X_m$。同时，由算法的安全性，$X$ 的下界也不大于 $x$，因此 $X$ 下界的可能值是有限的，上界同理，从而 $X$ 的区间也是有限半格。 += #empty + ```c + x = 1; // x: [1, 1] + while (x < 100) + { + // 第一次进入 x: [1, 1] + // 第二次进入 [2, 2] 与原值 [1, 1] 加宽合并，再与 [1, 1] 取并得到 x: [1, +infinity] + // 第三次进入 [2, 100] 与原值 [1, +infinity] 加宽合并，再与 [1, 1] 取并得到 x: [1, +infinity]，若不变窄则算法收敛 + // 若使用变窄算法，第四次进入 [2, 100] 与 [1, 1] 取并得到 x: [1, 100] + // 若使用变窄算法，第五次进入 [2, 100] 与 [1, 1] 取并得到 x: [1, 100]，算法收敛 + assert(x < 100); + // 第一次进入 x: [1, 1] + // 第二次进入将 [1, +infinity] 压缩到 [1, 99] + // 若使用变窄算法，第三次进入将 [1, +infinity] 压缩到 [1, 99] + // 若使用变窄算法，第四次进入将 [1, 100] 压缩到 [1, 99] + x++; + // 第一次进入 x: [2, 2] + // 第二次进入 x: [2, 100] + // 若使用变窄算法，第三次进入 x: [2, 100] + // 若使用变窄算法，第四次进入 x: [2, 100] + } + skip; + ``` + diff --git "a/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ" "b/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ" index 848568a..bd969fa 100644 --- "a/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ" +++ "b/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ" @@ -5,6 +5,7 @@ author: "YHTQ", date: datetime.today().display(), logo: none, + withChapterNewPage: true ) #let sup = math.union.sq = 前言 @@ -197,106 +198,239 @@ + 首先，基本块就是每两个 goto 语句之间的代码块 + 然后，基本块之间的跳转关系就是 goto 语句的目标 ] - #pagebreak() = 基于抽象解释的程序分析 == 数据流分析 - #definition[][ - 记 $A$ 为抽象域的集合，$X$ 为真实值的集合，记： - - $Gamma : A -> P(X)$ 将抽象域映射到真实值的集合 - - $alpha : X -> A$ 将具体值映射到抽象域，需要满足 $alpha(Gamma(a)) = {a}$ - ] - 所谓的数据流分析，就是要在带有条件，循环等控制流的程序中，处理类似前言中表达式正负的问题。数据流分析的常见手法是： - - 将全局状态（变量到值的映射）转换成抽象状态（变量到抽象值的映射） - - 为每个程序语句设计抽象状态函数，实时改变抽象状态 - #algorithm[抽象状态计算][ - - 对于一般的顺序语句，抽象状态函数是显然的 - - 对于条件语句，抽象状态函数是两个分支的抽象状态函数的上确界 - - 对于循环语句，考虑： - ```c - x = 100; - y = 1; - while (y > x) { - x *= -100; - y += 1; - } - ``` - 尽管我们不知道循环会执行多少次终止，从逻辑上我们仍然可以得到一些结果。为了实现，我们假设抽象域中有符号 $bot$ 使得 $Gamma(bot) = emptyset$，假设每个节点处符号的初始值都是 $bot$，从 entry 的后继节点开始，分析时随机选取节点使用分支合并更新状态，使用宽度优先方法，如果某节点更新就将其后继加入待更新节点，直至没有节点待更新。 - ] - #theorem[][ - 上面的算法是正确的，也即保证每个变量的值符合抽象状态。同时，它也保证停止，并且停止的结果与最开始选取的节点无关。 - ] - #remark[][ - 这种分析方法产生了以下几种不精确性： - - 将值抽象成有限个值的集合 - - 值的运算抽象到集合上，加大了不精确性 - - 发生分支时，往往事实上只有一个分支被执行，但我们假设两个都有可能执行 - - 状态合并时，也会产生不精确性 - ] - #example[可达定值分析][ - 给定程序，判断每个变量的值可能在哪些行被赋值。这与数据流分析很接近，其中具体域是所有程序行号，转换函数是在赋值语句处替换，其他语句不变。注意算法中需要初始将所有节点全部加入待更新节点，否则非赋值语句可能保持 $bot$ 不变，导致算法停止。 - ] - #example[可用表达式分析][ - 给定程序，如果从入口到某一位置 $p$ 的所有路径都计算了表达式 $e$，并且最后一次执行后没有改变与 $e$ 相关的变量，则称 $e$ 是 $p$ 处的一个可用表达式。这个问题中的具体域是程序中的所有表达式，每个节点的初始值是程序表达式的全集，转换函数是计算表达式时增加，变量赋值时删去相关的的表达式，分支合并时取交而非并。 - ] - #example[活跃变量分析][ - 给定程序，如果语句 $s$ 执行前，一个变量的值在 $s$ 或后续的语句仍然使用，则称之为活跃变量。与之前问题的主要区别在于我们需要倒着程序的执行顺序进行分析，抽象值含义是从当前位置开始任意长度的具体执行序列的集合（注意由于程序会无限执行，在倒着分析的时候不能假设所有的执行序列都在最后的节点终止）初始值为空集，每个节点处先删去写入的变量，再加入读取的变量，分支合并时取并。 - ] - #remark[][ - 一般来说，数据流分析只能考虑从 entry 开始或者从 exit 结束的有限执行序列。对于可能无穷的执行序列，逻辑上无法分析。对于活跃变量分析，我们可以转而证明在任意位置结束的有限执行序列都正确，进而保证时间上的正确性。 - ] - 一般而言，数据流分析有以下步骤： - - 设计抽象域 - - 编写节点转换函数，注意可能需要处理复杂表达式，此时可以对递归的表达式结构进行分析，或者直接对三地址码进行分析。 - - 处理控制流路径的分叉和合并 + === 基本数据流分析 + #definition[][ + 记 $A$ 为抽象域的集合，$X$ 为真实值的集合，记： + - $Gamma : A -> P(X)$ 将抽象域映射到真实值的集合 + - $alpha : X -> A$ 将具体值映射到抽象域，需要满足 $alpha(Gamma(a)) = {a}$ + ] + 所谓的数据流分析，就是要在带有条件，循环等控制流的程序中，处理类似前言中表达式正负的问题。数据流分析的常见手法是： + - 将全局状态（变量到值的映射）转换成抽象状态（变量到抽象值的映射） + - 为每个程序语句设计抽象状态函数，实时改变抽象状态 + #algorithm[抽象状态计算][ + - 对于一般的顺序语句，抽象状态函数是显然的 + - 对于条件语句，抽象状态函数是两个分支的抽象状态函数的上确界 + - 对于循环语句，考虑： + ```c + x = 100; + y = 1; + while (y > x) { + x *= -100; + y += 1; + } + ``` + 尽管我们不知道循环会执行多少次终止，从逻辑上我们仍然可以得到一些结果。为了实现，我们假设抽象域中有符号 $bot$ 使得 $Gamma(bot) = emptyset$，假设每个节点处符号的初始值都是 $bot$，从 entry 的后继节点开始，分析时随机选取节点使用分支合并更新状态，使用宽度优先方法，如果某节点更新就将其后继加入待更新节点，直至没有节点待更新。 + ] + #theorem[][ + 上面的算法是正确的，也即保证每个变量的值符合抽象状态。同时，它也保证停止，并且停止的结果与最开始选取的节点无关。 + ] + #remark[][ + 这种分析方法产生了以下几种不精确性： + - 将值抽象成有限个值的集合 + - 值的运算抽象到集合上，加大了不精确性 + - 发生分支时，往往事实上只有一个分支被执行，但我们假设两个都有可能执行 + - 状态合并时，也会产生不精确性 + ] + #example[可达定值分析][ + 给定程序，判断每个变量的值可能在哪些行被赋值。这与数据流分析很接近，其中具体域是所有程序行号，转换函数是在赋值语句处替换，其他语句不变。注意算法中需要初始将所有节点全部加入待更新节点，否则非赋值语句可能保持 $bot$ 不变，导致算法停止。 + ] + #example[可用表达式分析][ + 给定程序，如果从入口到某一位置 $p$ 的所有路径都计算了表达式 $e$，并且最后一次执行后没有改变与 $e$ 相关的变量，则称 $e$ 是 $p$ 处的一个可用表达式。这个问题中的具体域是程序中的所有表达式，每个节点的初始值是程序表达式的全集，转换函数是计算表达式时增加，变量赋值时删去相关的的表达式，分支合并时取交而非并。 + ] + #example[活跃变量分析][ + 给定程序，如果语句 $s$ 执行前，一个变量的值在 $s$ 或后续的语句仍然使用，则称之为活跃变量。与之前问题的主要区别在于我们需要倒着程序的执行顺序进行分析，抽象值含义是从当前位置开始任意长度的具体执行序列的集合（注意由于程序会无限执行，在倒着分析的时候不能假设所有的执行序列都在最后的节点终止）初始值为空集，每个节点处先删去写入的变量，再加入读取的变量，分支合并时取并。 + ] + #remark[][ + 一般来说，数据流分析只能考虑从 entry 开始或者从 exit 结束的有限执行序列。对于可能无穷的执行序列，逻辑上无法分析。对于活跃变量分析，我们可以转而证明在任意位置结束的有限执行序列都正确，进而保证时间上的正确性。 + ] + 一般而言，数据流分析有以下步骤： + - 设计抽象域 + - 编写节点转换函数，注意可能需要处理复杂表达式，此时可以对递归的表达式结构进行分析，或者直接对三地址码进行分析。 + - 处理控制流路径的分叉和合并 - 之前都没有讨论算法的终止性和合流性（节点选择顺序不影响结果），为此我们引入一套数据流分析的框架，并基于该框架进行证明。 - #definition[半格 semilattice][ - 称 $(S, sup)$ 为半格，如果满足： - - 幂等性：$x sup x = x$ - - 交换性：$x sup y = y sup x$ - - 非对称性：$$ - 不难验证，$x subset y := x sup y = y$ 是偏序关系。 + 之前都没有讨论算法的终止性和合流性（节点选择顺序不影响结果），为此我们引入一套数据流分析的框架，并基于该框架进行证明。 + #definition[半格 semilattice][ + 称 $(S, sup)$ 为半格，如果满足： + - 幂等性：$x sup x = x$ + - 交换性：$x sup y = y sup x$ + - 非对称性：$$ + 不难验证，$x subset y := x sup y = y$ 是偏序关系。 - 有最小值 $bot$ 的半格称为有界半格。 + 有最小值 $bot$ 的半格称为有界半格。 - 称一个有界半格的高度指其中全序子集元素个数的最大值。 - ] - #theorem[不动点定理][ - 给定有限高度的有界半格 $S$ 和单调函数 $f: S -> S$，则 $bot, f(bot), ..., $ 一定在有限步停止在 $f$ 的最小不等点 - ] - #proof[ - - 首先证明序列终止。不难验证： + 称一个有界半格的高度指其中全序子集元素个数的最大值。 + ] + #theorem[不动点定理][ + 给定有限高度的有界半格 $S$ 和单调函数 $f: S -> S$，则 $bot, f(bot), ..., $ 一定在有限步停止在 $f$ 的最小不等点 + ] + #proof[ + - 首先证明序列终止。不难验证： + $ + bot subset f(bot) => f(bot) subset f(f(bot)) => ... + $ + 说明该序列是链，而有限高度意味着链有限长，进而最终稳定，而稳定的值当然是不动点。 + - 其次，为了证明它是最小不动点，取 $x$ 是一个不动点，则： + $ + bot subset x => f(bot) subset f(x) = x => ... + $ + 反复应用可得结论 + ] + #definition[数据流单调分析框架][ + 可以定义一般框架： + - 一个控制流图 $G$ + - 一个有限高度的有界半格 $S$ + - 一个 entry + - 一个单调函数 $f$ + 可以证明，对于该框架（对应的随机选取节点进行更新的算法称为工单算法），依次选取节点更新的算法称为轮询算法），容易证明轮询算法一定收敛到更新函数的最小不动点，而工单算法也会收敛到该点，因此一定收敛并且收敛到相同值 + ] + #definition[分配性][ + 假设转换函数 $f_v$ 满足 $f_v (x) sup f_v (y) = f_v (x sup y)$，则称满足分配性。满足分配性的数据流分析不会因为提前合并引入不精确性。由集合交/并操作构造的转换函数都满足分配性。 + ] + === 数据流分析拓展：条件压缩 + 在上面的近似方案中，我们认为所有分支都会执行从而得到分析结果，这当然是荒谬的。为了使结果更精确，我们需要更精细地处理这个问题。一个常见的方案是增加条件压缩节点，也就是： + ``` + if (x > 0) + { + x += 1; + } + else + { + x = 1; + } + ``` + 转换成： + ``` + if (x > 0) + { + assert(x > 0); + x += 1; + } + else + { + assert(x <= 0); + x = 1; + } + ``` + 这里，我们的任务是要通过 assert 节点反解出 $x$ 满足的条件，这被称为*反向执行语义*。 + + 这里，我们拓展抽象域的定义以满足布尔值： + $ + {bot, T, F, top} + $ + #let Inv = $"Inv"$ + 其中 $gamma(bot) = {}, gamma(top) = {T, F}$，定义规则： + - $Inv(and) (bot) = (bot, bot)$ + - $Inv(and) (T) = (T, T)$ + - $Inv(and) (\_) = (top, top)$ + - $Inv(> 0)(bot) = bot$ + - $Inv(> 0)(T) = {x: "int" > 0}$ + - ... + 事实上，我们可以做更精确的压缩，结合目前已知的信息给出更精确的结果，例如： + $ + Inv(and) ((T, top), F) = (T, F) + $ + 其中前一个参数指变量当前的抽象状态，后一个参数指表达式的抽象值，结果是变量的新抽象状态。注意在实际的复杂表达式，例如： + $ + x > 0 and y > x and z > y = T + $ + 时，我们要先正向执行，得到： + $ + (x > 0, y > x, z > y): (top, top, top) + $ + 反向压缩得到： + $ + (x > 0, y > x, z > y): (T, T, T)\ + (x, y, z) : (>0, top, top) + $ + 不难看出这个过程并未终止，可以再次进行，迭代几次后可以得到： + $ + (x, y, z) : (>0, >0, >0) + $ + 一般的，如果反向执行的规则足够单调，则这样的迭代会收敛，然而实践上往也会使用不能保证收敛的反向执行语义。 + === 区间分析：加宽和变窄 + 对于下面的程序： + ```c + x = 1; + for (int i = 0; i < b; i++) { + x += 1; + } + ``` + 求出一个 $x$ 的上界和下界，这样的分析称为区间分析。实际结果为 $[0, +infinity]$ ，然而如果使用通常的数据流分析技术，我们无法真正得到 $+infinity$，或者说半格的高度是无穷的，导致无法收敛。有些时候，即使有限高度，高度也会过高导致收敛过慢。为此我们引入加宽和变窄的概念： + - 加宽：通过降低精度加快分析过程，包括： + - 简易加宽：降低格的高度，例如在上面的问题中，抽象域不取全体整数，而是例如： + $ + -infinity, 1, 2, ..., 100, +infinity + $ + 实际计算时，寻找与抽象域中格点接近的，保证正确的结果。尽管会导致精度损失，但安全性和收敛性往往容易保证。 + - 通用加宽：根据趋势猜测结果。具体来说，引入加宽算子 $a nabla b$，其中 $a$ 是该节点旧值，$b$ 是一轮更新后得到的新值，定义： + $ + [a, b] nabla [c, d] = (m, n) where\ + m = "if" c >= a "then" a "else" -infinity\ + n = "if" b <= d "then" b "else" +infinity + $ + 换言之，只要发现新结果的上界变大，就直接加宽到正无穷，否则采纳旧值（这里采纳旧值新值均可，采纳旧值可以更快收敛，采纳新值可能会造成无穷震荡）；下界变小，就直接加宽到负无穷。这样收敛的速度很快。不幸的是，加宽函数往往没有单调性，目前并没有容易判断的属性保证通用加宽的收敛性，在除了循环之外的场景往往也会导致奇怪的问题。实践上往往只会在循环的入口处使用通用加宽。 + - 变窄：加宽可以提高效率，然而往往会损失很多精确性。为此我们引入变窄技术，基本思想是在加宽收敛后，进行一轮普通的数据流分析，就可以得到较为精确的结果。 + #theorem[][ + 设普通数据流分析更新函数为 $F$（具有单调性），添加加宽算子后为 $G$ ，并且满足 $G(x) >= F(x)$，则加宽-变窄是安全的 + ] + #proof[ + 假设 $x_0$ 是 $F$ 的不动点，也就是当前抽象域下最精确的估计。不难发现： $ - bot subset f(bot) => f(bot) subset f(f(bot)) => ... + x <= x_0 => F(x) <= x_0 => G(x) <= x_0 $ - 说明该序列是链，而有限高度意味着链有限长，进而最终稳定，而稳定的值当然是不动点。 - - 其次，为了证明它是最小不动点，取 $x$ 是一个不动点，则： + 蕴含着 $G$ 是加宽是安全的。为了考虑变窄，假设加宽 $n$ 次后采取变窄，得到结果： $ - bot subset x => f(bot) subset f(x) = x => ... + F(G^n (bot)) $ - 反复应用可得结论 - ] - #definition[数据流单调分析框架][ - 可以定义一般框架： - - 一个控制流图 $G$ - - 一个有限高度的有界半格 $S$ - - 一个 entry - - 一个单调函数 $f$ - 可以证明，对于该框架（对应的随机选取节点进行更新的算法称为工单算法），依次选取节点更新的算法称为轮询算法），容易证明轮询算法一定收敛到更新函数的最小不动点，而工单算法也会收敛到该点，因此一定收敛并且收敛到相同值 - ] - #definition[分配性][ - 假设转换函数 $f_v$ 满足 $f_v (x) sup f_v (y) = f_v (x sup y)$，则称满足分配性。满足分配性的数据流分析不会因为提前合并引入不精确性。由集合交/并操作构造的转换函数都满足分配性。 - ] + ] + === 抽象解释 + #definition[][ + 假设具体域为 $D$，抽象域为 $A$ + 称 $gamma: A -> D$ 为具体化函数，$alpha: A -> D$ 为抽象化函数，称他们构成一个 Galois 连接，如果满足： + $ + alpha(X) <= Y <=> X <= gamma(Y) + $ + ] + #remark[][ + 事实上假设将偏序集看作范畴，一对 Galois 连接就是一对伴随函子。 + ] + #proposition[][ + $alpha, gamma$ 是 Galois 连接当且仅当以下性质全部成立： + - $forall X in D, X <= gamma (alpha(X))$ + - $forall Y in A. alpha(gamma(Y)) <= Y$ + - $forall X, Y in D, X <= Y => alpha(X) <= alpha(Y)$ + - $forall X, Y in A, X <= Y => gamma(X) <= gamma(Y)$ + ] + #definition[][ + 设 $alpha, gamma$ 是 Galois 连接，$f: A -> A, g: D -> D$，则： + - $f$ 是 $g$ 的安全抽象，如果： + $ + (alpha compose g compose gamma) (X) <= f(X) + $ + 也等价于： + $ + (g compose gamma) (X) <= (gamma compose f) (X) + $ + - $f$ 是 $g$ 的最佳抽象，如果： + $ + alpha compose g compose gamma = f + $ + - $f$ 是 $g$ 的精确抽象，如果： + $ + g compose gamma = gamma compose f + $ + 显然最佳抽象总是存在的，但精确抽象不一定存在。 + ] == 过程间分析 == 指针分析 - #pagebreak() = 基于约束求解的程序分析 == SAT == SMT == 符号执行 - #pagebreak() = 软件分析应用 == 程序合成 == 缺陷分析