5eqn

分类

PLT(11) 题解(12)

/ 注册

全部文章（共23篇）

CF242E XOR on Segment

有人向我反映在代码中写题解会令读者提升血压，我认为这种方式的优缺点如下：优点写起来方便，不需要切换界面便于写一段解释，放一段代码在代码中也便于顺着上面的注释继续讲解可以作为写代码的时候使自己思路清晰的一种手段缺点非常丑不支持 LaTeX\LaTeXLATEX 公式容易写着写...

C++

2023-01-23

0 444

Limit の线段树题单口胡题解 + 跳坑实录 Pt. 3

P3369 【模板】普通平衡树 #include <bits/stdc++.h> #include <functional> #define ll long long #define fori(n) for (ll i = 0; i < n; i++) #define ...

C++

2023-01-22

0 361

FStar 官方习题 Constructive & Classical Connectives

链接官网内容讲述了各种数理逻辑符号在 F* 里的原始实现，以及接近数学形式的 squashed form。提供了语法糖来书写用于操作 squashed form 的命题。个人感觉 F* 提供的语法糖相比 Lean 更冗长，使用体验也比较差，有种 Brainf**k 的感觉习题一大意...

2023-01-22

0 285

FStar 官方习题 Equality Types

可参考官网内容讲述了不同的等价关系，例如定义相等由于采用 Inductive Type 机制，原先表现形式不同的表达式经过自动化简后程序无法区分例 (fun x -> x) a 和 a (factorial 3) 和 6 证明相等使用 equal a b 这个类型...

2023-01-22

0 301

Codeforces Round #845 现场题解 A, B, D

这些题解是边做题边打的，因此较为省略，旨在尝试让自己讲明白题目是否能起到贯通思路、减少错误的作用。 A. Everybody Likes Good Arrays! 大意求最少操作次数使得相邻元素奇偶性不同，操作为将两个相邻且奇偶性相同的元素合并为乘积。思路相同奇偶性乘法不改变奇偶性，所以贪...

C++

2023-01-22

1 646

Limit の线段树题单口胡题解 + 跳坑实录 Pt. 2

P1908 逆序对题意求逆序对的数量。数组的元素可以非常大。思路离散化后使用权值线段树即可。个人理解，权值线段树本质上是使用线段树维护元素出现数量的数据结构，和线段树没有本质区别。坑加入最大元素时，不要进行区间长度为 0 的查询！会 RE！ AC 代码 #include <bi...

C++

2023-01-21

0 452

FStar 官方习题 Length-indexed Lists

可参考官网。内容可以将类型的一些属性作为类型的编号，这样在递归定义类型时就可以将属性直接计算出来。例如，以下是定长数组的定义： type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:...

F*

2023-01-21

0 359

FStar 官方习题 Case Study: Quicksort

概要这一小节讲述了如何用 F* 实现快排算法，并且证明其确实有排序的功能。铺垫：快排实现递归计算 list 长度： let rec length #a (l:list a) : nat = match l with | [] -> 0 | _ :: tl ->...

F*

2023-01-20

0 413

Limit の线段树题单口胡题解 + 跳坑实录 Pt. 1

P3372 【模板】线段树 1 使用最基本的线段树即可。遇到的坑内存要开够，考虑直接采用 N << 2 build 和 add 的时候都要 push_up add 和 query 的时候都要 push_down r - l == 1 不要写成 l - r == 1 P3373 【...

C++

2023-01-20

0 391

FStar 官方习题 Lemmas and proofs by induction

FStar 是什么？ F* 是一种面向证明的编程语言，运用大量奇技淫巧实现程序自证明，例如：依值类型，Dependent Type，简而言之就是允许类型依赖于具体的值函数式编程，Functional Programming，函数是一等公民，能像值一样作为参数和返回值元语言，Meta Lang...

F*

2023-01-19

1 361