Programming Languages Assignment 2: Lambda Theory

点击此处下载 PDF

Programming Languages Assignment 1: JSafe

点击此处下载 PDF

德语 Notes

动词变位

“sein” 的动词变位

“heißen” 的动词变位

• Woher kommst du? 你从哪里来?
  Woher kommen Sie?
• Ich komme aus China. 我来自中国.
  Ich komme aus Deutschland.
  Ich komme aus den USA.

规则变化里的特殊情况

• “arbeiten” 的动词变位

• 其他动词：
  • tanzen: du tanzt
  • reisen: du reist
  • öffnen: du öffnest
  • regnen: es regnet （下雨）

不规则变化

• 变音动词（a → ä）
  fahren - du fährst
  schlafen - du schläfst
  laufen - du läufst

• 换音动词（e → i 或 e → ie）
  geben - du gibst
  sehen - du siehst
  nehmen - du nimmst

命令式

第二人称，换音动词保留，变音动词变回原形。

代词和限定词

人称代词

• 第一格

• 第四格

• 第三格

反身代词：表示主语和宾语为同一。
第三人称和尊称用 sich 表示。

限定词

定冠词的变格 (der-Wort)

其他包括：

• 定冠词：der, die, das
• 指示代词：dies-, jen-, solch-
• 不定代词：all-, beid-, manch-
• 疑问代词：welch-

不定冠词的变格 (kein-Wort)

其他包括：不定冠词、否定词、物主代词。

名词的格

第一格 (Der Nominativ)

1. 主语
   Der Student lernt Deutsch.

2. 系表结构
   Das ist ein Tisch.

第四格 (Der Akkusativ)

1. 直接宾语
   Ich habe einen Tisch.

2. es gibt 表示存在
   Es gibt einen Tisch da drüben.

3. 时间状语：jeden Tag, letzen Sommer, den ganzen Tag, diesen Abend

4. 要求第四格宾语的介词：

   • für - 为了…
   • um - 围绕着
   • gegen - 朝着
   • durch - 穿过
   • ohne - 没有

第三格 (Der Dativ)

1. 间接宾语
   Ich gebe der Frau ein Buch.
   (第三格名词 der Frau 出现在第四格名词 ein Buch 之前)
   Er schenkt es mir. （双宾语句中，第四格较短的宾语放前）

2. 受益（害）者
   Wir kaufen unserer Mutter ein Geschenk.
   (Mutter 是受益者)
   Hilf mir, bitte!

3. 表示主观感受
   Mir ist kalt. / Es ist mir kalt. (我觉得冷)
   Der Film gefällt mir. (我喜欢这部电影)
   Das Hemd steht mir. (这件衬衫很适合我)
   Es tut mir leid. (对不起)

4. 带第三格宾语的介词

   • aus: 从……来
     Ich komme aus China.
     Ich gehe aus der Schule.
   • außer: 除了……以外
     Außer mir gehen alle schwimmen.
   • bei: 跟人表示地点，跟物表示条件
     Bei Frau Schmidt ist es immer sehr laut.
   • mit: 和……一起，用……
     Ich gehe mit meiner Mutter nach Hause.
   • nach: 在……之后，去……
     Mutti geht erst nach der Arbeit nach Hause.
   • seit: 自从……
     Hans wohnt seit einem Jahr in China.
   • von: 所有者
     Das ist ein Buch von meinem Vater.
   • zu: 强烈目的性地去……
     Gehst du zur Schule?
   • gegenüber: 在……正对面
     Dem Haus gegenüber steht ein Baum.

可三可四的介词

可三可四的介词需要根据动作的静态或动态来决定格的使用，称为“静三动四”。

• 常见介词：
  • an: 在……（垂直接触）
    Am Montag habe ich keinen Deutschunterricht.
    Ich denke an dich.
  • auf: 在……（水平接触）
    Auf dem Bett liegen drei Socken.
    Ich warte auf dich.
  • hinter: 在……后面
  • in: 在……内部
  • neben: 在……旁边
  • über: 在……上方
  • unter: 在……下面
  • vor: 在……前面
  • zwischen: 在……之间

形容词词尾变化

形容词词尾的变化依赖于以下因素：是否有冠词、冠词是否变化、名词是否单数、冠词是否表明性别。

5. 形容词的升级

原级

• so/genauso/ebenso + Adj. + wie: 与……一样
  Er ist genauso alt wie ich. (他和我一样老)

• nicht so + Adj. + wie: 不如……
  Vera ist nicht so alt wie ich. (Vera 不如我老)

比较级和最高级

• 规则变化
  比较级加 -er，最高级加 -st。
  klein → kleiner → kleinst
  billig → billiger → billigst
  schwer → schwerer → schwerst

• 特殊变化

  1. 单音节元音为 a, o, u 的形容词需要变音：
     arm → ärmer → ärmst
     groß → größer → größt
     jung → jünger → jüngst

  2. 元音和辅音同时变化：
     hoch → höher → höchst
     nah → näher → nächst

  3. 以 -d, -s, -sch, -ß, -t, -tz, -x, -z 结尾的形容词最高级加 -est：
     wild → wilder → wildest
     hübsch → hübscher → hübschest

  4. 不规则变化：
     gut → besser → best
     viel → mehr → meist
     gern → lieber → liebst
     oft/häufig → häufiger → häufigst

• 形容词比较级的用法

  • 肯定形式：Adj.-er + als
    Er ist langsamer als seine Schwester. (他比他妹妹慢)
  • 否定形式：nicht + Adj.-er + als
    Er ist nicht langsamer als seine Schwester. (他不比他妹妹慢)

• 最高级的用法

  1. 定冠词 + Adj.-st + Nomen + 范围：
     Er ist das größte Kind in der Klasse. (他是班上最高的孩子)
  2. einer/eine/eines + der + Adj.-sten + Nomen (复数) + 范围：
     Marilyn Monroe ist eine der schönsten Frauen Amerikas. (玛丽莲·梦露是美国最美的女人之一)

定代词和不定代词

定代词

定代词需重读，常放在句首，通过格来确定语义，语序无关。
Schau mal, hier sind Esstische. Wie findest du den hier?
Den finde ich nicht schön. Der ist zu groß.

不定代词

• 若宾语位置空缺，可用不定代词填充：
  Schau mal! Hier sind Lampen. Hast du schon welche?
  Nein, ich habe noch keine.

点击此处下载 PDF

程序合成

经典程序合成定义

输入:

1. 一个程序空间, 通常用文法表示.
2. 一条规约, 通常为逻辑表达式.

输出: 一个程序, 满足.

一个例子: max问题

语法:

规约: .

期望答案为: .

程序合成方法

1
2
3
4

graph LR
	A[生成程序] --程序--> B[验证正确性]
	B --正确--> 输出
	B --错误--> A

1. 如何产生下一个被搜索的程序?

   1. 枚举法——按照固定格式搜索.
   2. 约束求解法——转成约束求解问题.
   3. 空间表示法——一次考虑一组程序而非单个程序.
   4. 基于概率的方法——基于概率模型查找最有可能的程序.

2. 如何验证程序的正确性? 抽象解释, 符号执行.

   1. 基于反例的优化: CEGIS. 保存约束求解器的反例, 首先采用测试. 要选择一个好的反例, 就要估算它可以排除的程序的个数.
   2. LearnSy: 通过近似输出相同的程序对的个数来估计被排除的程序. 输出相同的程序对越多，被一个输入输出对排除的程序期望数量就越少.
   3. …

枚举 （enumerate）

Z3的安装和使用

Windows上的安装

可以直接在Z3的GitHub主页上下载对应版本的，然后直接配置路径即可。

使用下面的命令检查是否安装成功：

1

z3 --version

如果安装成功了会显示z3的版本信息。

Z3的使用

Z3使用SMTLIB格式。具体的可以学习：Introduction | Online Z3 Guide。这是一种类似于Lisp的语言。关于Lisp，我推荐学习SICP(Structure and Interpretation of Computer Science)。

基本命令

基本运行方法

打印：(echo "starting z3...")。

声明常量：(declare-const a Int)。

声明函数：(declare-fun f (Int Bool) Int)。

如果你在example.smt2文件中写入下面的代码（我这里就使用Lisp的高亮了）：

1
2
3

(echo "starting Z3...")
(declare-const a Int)
(declare-fun f (Int Bool) Int)

并且运行：

1

z3 example.smt2

你应该可以看见：

1

starting Z3...

被打印出来了。

求解SAT问题

下面我们介绍Z3中比较重要的几个命令：

添加约束：(assert (< a 10))。

判断是否可满足（satisfiable）：(check-sat)。

要求给出可满足的一个赋值：(get-model)。

1
2
3
4
5
6

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (< a 10))
(assert (> (f a true) 100))
(check-sat)
(get-model)

对于这段代码实际上就是在求解下面这个SAT问题是否可满足：

对于这个问题，Z3给出的答案是：

1
2
3
4
5
6
7

sat
(
  (define-fun a () Int
    0)
  (define-fun f ((x!0 Int) (x!1 Bool)) Int
    101)
)

这里的常量实际上也是一个函数，它不接受任何的参数，返回一个Int类型的数字。上面的解答意味着我们的SAT问题是可满足的，同时一个可满足的赋值为：

设置作用域（Scopes）

push命令将会创建一个新的作用域，里面存储着所有全局的定义、约束等。

pop则将会将作用域里所有的语句弹出。

1
2
3
4
5
6
7
8
9
10
11
12
13
14

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(push)
(assert (= (+ x y) 10))
(assert (= (+ x (* 2 y)) 20))
(check-sat)
(pop) ; remove the two assertions
(push) 
(assert (= (+ (* 3 x) y) 10))
(assert (= (+ (* 2 x) (* 2 y)) 21))
(check-sat)
(declare-const p Bool)
(pop)

配置Z3（Configuration）

使用set-option，下面是一个例子：

1
2
3
4
5
6
7
8
9
10

(set-option :print-success true)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-const x Int)
(assert (= x 1))
(set-option :produce-proofs false) ; error, cannot change this option after an assertion
(echo "before reset")
(reset)
(set-option :produce-proofs false) ; ok

其他命令

(display t)会把式子变得漂亮一点，(simplify t)则会化简式子。

(define-sort [symbol] ([params_type]+) [sort])表示创建一个新的数据类型。

1

(define-sort List-Set (T) (Array (List T) Bool))

就会创建一个类型List-Set，这个类型要求一个参数T，并且返回一个类似于Map的数据类型。

命题逻辑（Propositional Logic）

Z3中已经预先定义好了Bool类型，并且支持and、or、xor、=>、ite(if-then-else)、=(实际上意味着)。

1
2
3
4
5
6
7
8

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(define-fun conjecture () Bool
	(=> (and (=> p q) (=> q r))
		(=> p r)))
(assert (not conjecture))
(check-sat)

define-fun实际上定义了一个Macro。

如果要证明一个公式，也就是证明总是为真的，那么我们就要说明总是为假的，也就是说明是一个不可满足的公式。

不可满足的核心（Unsatisfiable Cores）

1
2
3
4
5
6
7
8
9
10
11
12

(set-option :produce-unsat-cores true)
(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)
(declare-const t Bool)
(assert (! p :named +p))
(assert (! q :named +q))
(assert (! r :named +r))
(assert (! (not (or p q)) :named -p-or-q))
(check-sat)
(get-unsat-core)

我们在这里把公式取了一个名字为+p。

1
2

unsat
(+q -p-or-q)

最后发现产生矛盾的核心集是：。

未解读的函数和变量

我们完全可以扔给Z3一些它不知道什么含义的函数和变量，让它计算出一个理论，使得约束满足。

例如：

1
2
3
4
5
6
7
8
9

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)

代表约束：

Z3给出的结果是：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

sat
(
  ;; universe for A:
  ;;   A!val!1 A!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!1 () A)
  (declare-fun A!val!0 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!1) (= x A!val!0)))
  ;; -----------
  (define-fun x () A
    A!val!0)
  (define-fun y () A
    A!val!1)
  (define-fun f ((x!0 A)) A
    (ite (= x!0 A!val!1) A!val!0
      A!val!1))
)

这个解读代表着：类型有两个基本的元素和，同时有。然后Z3给出了这个问题的一个可能的赋值：

创建新的类型

可以参看 Lisp 的语法。

理论（Theory）

理论大约等于一组公理。

Z3支持的理论有：Arithmetic、Bitvectors、IEEE Floats、Arrays、Datatypes、Strings、Sequences、Sequences、Regular Expressions、Unicode Characters、Special Relations。

Arithmetic

策略（Strategies）

这个其实和 Coq证明器有点像，请参看Software Foundations。

Fast and Accurate Flow-Insensitive Points-To Analysis

• [1](Marc Shapiro and Susan Horwitz. 1997. Fast and accurate flow-insensitive points-to analysis. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ‘97). Association for Computing Machinery, New York, NY, USA, 1–14. https://doi.org/10.1145/263699.263703)

原先的Steensgaard算法要求当一个节点的出度的时候就合并. [1]中的方法则是:

1. 当节点的出度的时候, 再合并.
2. 把所有的节点分为类.
3. 可以多运行几次, 改变划分的方法, 合并最精确的.

Welcome to Hexo! This is your very first post. Check documentation for more info. If you get any problems when using Hexo, you can find the answer in troubleshooting or you can ask me on GitHub.

Quick Start

Create a new post

1

$ hexo new "My New Post"

More info: Writing

Run server

1

$ hexo server

More info: Server

Generate static files

1

$ hexo generate

More info: Generating

Deploy to remote sites

1

$ hexo deploy

More info: Deployment