# 蕴涵词的解释

命题逻辑的第一个难点就是蕴涵词的解释。尽管逻辑教材提供了大量解释，但是很少有人提供一个更直接的理解方式。这里，我尝试从单调推理的角度直接推理出蕴涵词的真值表。

命题逻辑的第一个难点就是蕴涵词的解释。尽管逻辑教材提供了大量解释，但是很少有人提供一个更直接的理解方式。这里，我尝试从单调推理的角度直接推理出蕴涵词的真值表。

Rust is generally believed to be undefined-behavior-free when you write the entire program in safe Rust. However, this turns out false, and has a profound relationship with the Halting Problem.

Emacs is an advanced text editor, which has great support for programming. Let's face it: not every language has been supported by the ecosystem. There are times you have to write your own major mode.

I was always wondering how to deal with `Error`

s in Rust in a better way. Rust seems to encourage one-module-one-Error style, and you have to compose `Error`

s before writing any code.

Let's face it: this is good, but not very good. What can a programmer tell from the following signature?

```
fn transfer(alice: Account, bob: Account) -> Result<(), BankError>;
```

So... This function *could* return an error, but we don't know *what* could be returned. Let's take a look at the definition of `BankError`

.

```
enum BankError {
AccountNotFound,
DatacenterOffline,
ClerkNotOnDuty,
ServerOnFire,
...
}
```

So, which of them could be returned? Without looking at (read, digging into) the source code, one cannot tell with confidence.

Also, for quick'n'dirty jobs, Rustaceans are forced to take a hard way to compose an `Error`

type, or try hard to make use of an existing one... Why can't we just compose freely what we want?

All of the problems boil down to the problem of the extensibily of the Error type. This turns out to be a long standing problem, called the Expression Problem.

```
How can you add variants to a data type, without recompiling other parts of the program?
```

Functional Pearls gave an awesome answer, presented in the paper "Data types à la carte". Let's see how it works.

```
data Expr f = In (f (Expr f))
data Val e = Val Int
data Add e = Add e e
```

Wait. What does that mean? I don't know yet... `Expr`

looks like a random fixed point, while `Val`

and `Add`

are supposed to be the variants of `Expr`

.

`Val`

and `Add`

turn out (unsurprisingly) to be `Functor`

s.

```
instance Functor Val where
fmap _ (Val x) = Val x
instance Functor Add where
fmap f (Add e1 e2) = Add (f e1) (f e2)
```

So the type parameter `e`

reflects the substructure. To compose them, we need more facility:

```
infixr 6 :+:
data (f :+: g) e = Inl (f e) | Inr (g e)
instance (Functor f, Functor g) => Functor (f :+: g) where
fmap f (Inl x) = Inl $ fmap f x
fmap f (Inr y) = Inr $ fmap f y
```

Since `Expr`

is a nested structure, we need some way to "walk" it.

```
foldExpr :: Functor f => (f a -> a) -> Expr f -> a
foldExpr f (In t) = f (fmap (foldExpr f) t)
```

`f`

is an F-algebra. `f a -> a`

specifies one step of recursion. To interpret `Val`

and `Add`

,

```
instance Eval Val where
evalAlgebra (Val x) = x
instance Eval Add where
evalAlgebra (Add x y) = x + y
instance (Eval f, Eval g) => Eval (f :+: g) where
evalAlgebra (Inl x) = evalAlgebra x
evalAlgebra (Inr y) = evalAlgebra y
eval :: Eval f => Expr f -> Int
eval expr = foldExpr evalAlgebra expr
```

We can't yet make everything go. In the definition of `Expr`

, the structure looks like `f (Expr f)`

, so the inner type and outer type must match. We need some way to promote it. Take inspiration from the `From`

trait of Rust.

```
class (Functor sub, Functor sup) => sub :<: sup where
inj :: sub a -> sup a
instance Functor f => f :<: f where
inj = id
instance (Functor f, Functor g) => f :<: (f :+: g) where
inj = Inl
instance (Functor f, Functor g, Functor h, f :<: g) => f :<: (h :+: g) where
inj = Inr . inj
inject :: (g :<: f) => g (Expr f) -> Expr f
inject = In . inj
```

Now everything should work, but using such types is quite painful, let's make some smart constructors.

```
val :: (Val :<: f) => Int -> Expr f
val x = inject (Val x)
infixl 6 ⊕
(⊕) :: (Add :<: f) => Expr f -> Expr f -> Expr f
x ⊕ y = inject (Add x y)
```

Let's try:

```
eval (val 1 ⊕ val 2)
```

As long as you have followed along, you should have noticed that, we can compose the variants pretty easily:

```
Expr Val
Expr Add
Expr (Val :+: Add)
```

Isn't this what we wanted? Let's apply this idea to error types!

```
foldError :: Functor f => (f a -> a) -> Error f -> a
foldError f (In t) = f (fmap (foldError f) t)
injectError :: (g :<: f) => Error g -> Error f
injectError = foldError inject
class Functor f => Report f where
reportAlgebra :: Report g => f (Error g) -> String
instance (Report f, Report g) => Report (f :+: g) where
reportAlgebra (Inl x) = reportAlgebra x
reportAlgebra (Inr y) = reportAlgebra y
report :: Report f => Error f -> String
report (In t) = reportAlgebra t
data Success f = Success deriving (Show, Functor)
data Result a f = Result a deriving (Show, Functor)
data BadCode f = BadCode Int deriving (Show, Functor)
data UserError f = UserError String deriving (Show, Functor)
instance Report Success where
reportAlgebra Success = "Success"
instance Report BadCode where
reportAlgebra (BadCode x) = "Bad code (" ++ (show x) ++ ")"
instance Report UserError where
reportAlgebra (UserError msg) = "User error: " ++ msg
instance Show a => Report (Result a) where
reportAlgebra (Result x) = "Result: " ++ show x
success :: (Success :<: f) => Error f
success = inject Success
badCode :: (BadCode :<: f) => Int -> Error f
badCode code = inject (BadCode code)
userError :: (UserError :<: f) => String -> Error f
userError msg = inject (UserError msg)
result :: (Result a :<: f) => a -> Error f
result r = inject (Result r)
liftEither :: (g :<: f) => Either (Error g) a -> Either (Error f) a
liftEither (Left x) = Left (injectError x)
liftEither (Right y) = Right y
mapLeft :: (a -> c) -> Either a b -> Either c b
mapLeft f (Left a) = Left (f a)
mapLeft f (Right a) = Right a
from :: (g :<: f) => (a -> Either (Error g) b) -> a -> Either (Error f) b
from f x = liftEither (f x)
checkInt :: Int -> Either (Error BadCode) Int
checkInt x = if x < 0 then Left (badCode x) else Right x
checkString :: String -> Either (Error UserError) Int
checkString s = if length s > 10 then Left (userError "string too long") else Right (length s)
job :: Int -> String -> Either (Error (BadCode :+: UserError)) Int
job x y = do
x <- from checkInt x
y <- from checkString y
return (x+y)
```

There is still a small annoyance, that one has to convert `from`

a lower error type to a higher one, but overall this looks pretty neat.

`Expr`

is a fixed point operator, and `Expr Val`

is the fixed point of `Val`

. The type of a value like `Val 9`

is actually `Val e`

where `e`

is free. By wrapping it with `Expr`

, the `e`

now disappears, and the type of the whole expression is now closed. `foldXX`

is actually catamorphism: The fixed point operator gives us an initial F-algebra $(\mu F, In_F)$, and for any F-algebra $(X,\phi)$, there exists a catamorphism from $\mu F$ to $X$. The definition of `foldExpr`

seemed like magic out of air, but it's so obvious, looking at the following commutative diagram.

$$\require{amscd} \begin{CD} F (\mu F) @>{In_F}>> \mu F\ @V{F (\text{cata}~\phi)}VV @VV{\text{cata}~\phi}V\ FX @>>{\phi}> X \end{CD}$$

Catamorphism is the generalized `fold`

(that's why we call it `foldXXX`

here), which is used to destroy the structure: what we have is a $\mu F$ (like, `Expr (Val :+: Add)`

), and we want a final result (`Int`

), then by finding an algebra `(Val :+: Add) Int -> Int`

, we can get for free a catamorphism `Expr (Val :+: Add) -> Int`

. By writing a few typeclasses, we can compose types easily, and they gradually build up the algebra we want.

How did the authors find this solution? I should say I don't know, but my guess is that at first they separated the cases out and found a way to compose them, then their knowledge of recursion schemes (F-algebra) helped.

In the original "Data types à la carte" paper, free `Monad`

s can also be composed. Read it if you are interested.

Unfortunately, error handling has more to do with software engineering than stupid type checking. I might not use this approach in the future. Just do what others do!

面向对象语言为编程语言引入了所谓的子类型系统，简单说就是“猫是动物”、“狗是动物”，小类型（猫）可以被当作大类型（动物）用。但是对于函数本身，却有一个奇怪的不对称。

Have you ever wondered is there a way to compute without ever revealing the inputs? For example, you can use a mobile phone to navigate, without the server knowing where you actually are!

It is truly intriguing and has occurred to me several times. This problem, while easy to understand on the surface, turns out harder than I expected at first. I believe it's been studied extensively by crypto experts, but I know little about crypto so I don't even know the keyword to search with. I'll appreciate it if somebody could tell me something about this...

Nevertheless, I will describe my attempt below.

Intuitively: How to compute (evaluate a function) without the computer knowning the inputs?

One way to achieve this is to simply encrypt the input with a (public) key, and different users shall have different keys, so that the computer wouldn't have the chance to ever reveal the plaintext inputs. (I'd like to point out here, this is just one way I came up with upon, on which the rest of this article is based, and there might be other ways that I didn't think of.)

Simply put, given a function $f(x)$, an encryption algorithm $E(x)$, and a decryption $D(x)$, we would like to find a function $F(x)$, satisfying $D(F(E(x))) = f(x)$, where $E(x)$ and $D(x)$ depend on the user (the input provider). Since $E(x)$ and $D(x)$ should adopt the same encryption scheme, $D(E(x)) = x$ holds. Note that I intentionlly leave some details undefined.

It's easy to show that, if we could find a standardized procedure to find such a function $F$ for all $D(x)$ and $E(x)$, we would have solved this problem perfectly. However, this task is too terrifying, isn't it? I would be completely satisfied if I could find a solution when a specific encryption scheme is given.

Firstly, let's think about the trivial cases: what if $E(x)$ and $D(x)$ do absolutely nothing?

$$E(F(D(x))) = F(x) = f(x)$$

Not bad, no?

Similarly, if $f$ does nothing:

$$E(F(D(x))) = f(x) = x$$

We can just take $F(x) = x$.

Simple cases are not really simple, as you can build a Turing machine if it contains sufficiently powerful operations. I would like to know if we can build an adder with this "secure computation" thing. Let's start with NOT.

First consider only the symmetric XOR encryption, and let the variable $x$ to be boolean. The key is also boolean.

The original NOT function is defined as $f(x) = 1-x$, which negates the boolean variable. Simple truth-table computations show that, well, it's actually feasible! We can take $F(x) = x$.

The same reasoning can be applied to any $n$-bit vector easily.

Now we've got NOT, let's see if we can solve for AND.

Here comes the first problem: how to represent a binary function? Easy, make the function take one argument which is a 2-bit vector, whose result is boolean. Unfortunately, this naive approach will get in the way of encryption, as encryption takes 2 bits as key, while the output only needs 1 bit, breaking the symmetry. But worry not, since both the key and the 1-bit vec can be padded to 2 bits, there is no problem.

Different from the 1-bit case, this time the truth table is much bigger. I didn't bother to check by hand, and just verified the assertion with Z3, which happens to support binary functions.

```
from z3 import *
x1, x2 = Bools('x1 x2')
k1, k2 = Bools('k1 k2')
F = Function('F', BoolSort(), BoolSort(), BoolSort())
s = Solver()
s.add(ForAll(x1,
ForAll(x2,
ForAll(k1,
ForAll(k2,
Xor(F(Xor(x1, k1), Xor(x2, k2)), k2) == And(x1, x2))))))
if s.check() == sat:
print(s.model())
```

Since we pad consistently, the decryption only uses `k2`

. What if we
use asymmetrical XOR, where decryption uses an arbitrary function that
fuses `k1`

and `k2`

together? Well, see for yourself, still no
solution. What if we relax the condition, and only uses 1-bit key?
While I strongly doubt the security and usefulness of such a crypto
system, unfortunately, no solution found. Code:

```
from z3 import *
x1, x2 = Bools('x1 x2')
k = Bool('k')
F = Function('F', BoolSort(), BoolSort(), BoolSort())
s = Solver()
s.add(ForAll(k, ForAll(x1, ForAll(x2, Xor(F(Xor(x1, k), Xor(x2, k)), k) == And(x1, x2)))))
if s.check() == sat:
print(s.model())
else:
print('infeasible')
```

AND is just too powerful, I guess. :-/ Or maybe the universe just forbids us doing such kind of "secure computation"...

From the constraint $E(F(D(x))) = f(x)$, we can conclude $F$ can preserve some information from $D$, and the information about private key is cancelled out by $E$.

I worked on the maths (omitted) when $f(x) = x + c$, but I don't know how to cancel out the private bits.

Z3 is a sophisticated SMT solver, which can solve large models in seconds. Z3 comes with its own Sexp-based DSL, but it's very quirky, so I used the Python binding. Well, it still sucks. Hey, maybe you could design a better DSL!

Generally speaking, we don't have to deal with arbitrarily large numbers, so I drove Z3 to check if there are any solutions when we only consider n-bit vector and don't specify a crypto (let z3 figure it out instead).

```
from z3 import *
def check(sz, f):
x, k = BitVecs('x k', sz)
k1, k2 = BitVecs('k1 k2', sz)
F = Function('F', BitVecSort(sz), BitVecSort(sz))
E = Function('E', BitVecSort(sz), BitVecSort(sz), BitVecSort(sz))
D = Function('D', BitVecSort(sz), BitVecSort(sz), BitVecSort(sz))
s = Solver()
s.add(ForAll(x, ForAll(k,
And(D(k, E(k, x)) == x, # (1)
E(k, F(D(k, x))) == f(x))))) # (2)
s.add(Not(ForAll(k1, ForAll(k2, ForAll(x, E(k1, x) == E(k2, x)))))) # (3)
if s.check() == sat:
print(s.model())
check(1, lambda x: 1-x) # f(x) = Not(x)
```

Constraints explained:

- Decrypting a encrypted message will return you the plaintext.
- What "secure computation" is all about.
- Rule out trivial cases, where
`E`

and`D`

don't depend on the key at all.

(Constraint 3 tells us coding z3 is not as easy as it seems. Z3 will happily accept your formulae, but the validity remains unchecked for your specific scenarios. You just don't get it right easily. Actually, there were some bugs in my first attempt, and they weren't discovered until I started writing this article. Z3 is indeed a great listener...)

Believe it or not, this piece of code can automatically solve the
problem at hand, giving you a solution when one is found, or reporting
unsat when no solution is possible. However, it can take centuries to
finish when `sz`

is large.

Running the script above gives back the simple case we analyzed
before: `D(k,x) = E(k,x) = k^x`

, and `f(x) = not x`

. Magic, right?

There are two problems with this approach.

- The crypto is not flexible, as it comes "bundled" with the function
we want to evaluate. This could lead z3 to finding an
`E`

or an`D`

that encodes the computation in itself with`F`

being a no-op. Absolutely against our will. - The crypto is symmetrical. To make it asymmetrical, we must write down the relation between a public key and a private key, in the language of first-order logic.

This is an (unfinished) attempt, on which I spent about two hours of
my spare time. There are still hundreds of problems yet to be solved
or even proposed. Like, we know `F`

must preserve information about
`D`

, but how much? Which class of functions can have solutions?

What about RSA? What about AND? Maybe our universe just forbids us doing such kind of computation, but there might be other ways around, I don't know.

I believe this topic has been extensively studied. Garbled circuits seem to be relevant, but I haven't understood the Wikipedia page on that subject so I can't say for sure...

汉诺塔问题是一个简单的问题，它有一个简明易懂的递归解法，常常被用来当作递归的入门教程。前几天，有个水群里有人在想怎么写非递归的汉诺塔，然后写了用栈模拟的递归做法说它是非递归的……虽然倒也不是不能这么理解，但是显然，对于汉诺塔这种简单的问题，我们应该可以做得更好。

不久前偶然翻出来去年写的纯粹数学前沿的课程作业，当时刚看完《Quantum Mechanics: The Theoretical Minimum》，所以写的是简单的量子力学。因为是赶制出来的，内容也不是很详细（比如甚至连密度矩阵都没提），主要是强调特征值。感觉作为简单的量子力学总结/入门可能有点用？所以就把 LaTeX 改写成 Markdown 发到博客上了。~~有点凑数之嫌~~

标题是故意这么写的，强调我完全不懂量子力学。[滑稽.jpg]

这篇文章的话题是「依赖类型」。很多人，甚至是写过多年程序的人，可能都没有接触过这个概念。简单说，如果一个类型**依赖于一个不是类型的东西**，那它就是依赖类型。其实我本人是这个话题的门外汉，那我怎么想起来写这样的一篇文章了呢？因为我刚刚读完《The Little Typer》，感觉非常新奇有趣，所以想写一写。如果我能把这份乐趣分享给你，那我会很高兴的～ (^_^)

This post is about **GNU Emacs**. There are so many articles written
for beginners, but I'm often dissatisfied and frustrated by their
selection of materials. I believe, to use Emacs, you don't have to be
a genius. Getting started with Emacs should be as easy as using
Notepad!