蕴涵词的解释

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

How to write an Emacs major mode

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.

Error types à la carte

The problem with closed Error types

I was always wondering how to deal with Errors in Rust in a better way. Rust seems to encourage one-module-one-Error style, and you have to compose Errors 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?

Data types à la carte

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 Functors.

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)

Error types à la carte

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.

In retrospect

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 Monads 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!

Secure Computation, An Attempt

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.

Problem Statement

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.

Trivial

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$.

1-bit, XOR, Not

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.

2-bit, XOR, And

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"...

RSA

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 to rescue

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:

  1. Decrypting a encrypted message will return you the plaintext.
  2. What "secure computation" is all about.
  3. 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.

  1. 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.
  2. 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.

Conclusion

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》,感觉非常新奇有趣,所以想写一写。如果我能把这份乐趣分享给你,那我会很高兴的~ (^_^)

A Sane Introduction to Emacs

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!