GaeBlogX Arista Networks, Software-Defined Networking

SeraphRoy's Blog

Notes, Word Salad, etc.
• Jekyll Search Solutions

2019-01-20
Yanxi Chen

终于我找到了这个。 但是这个其实充满了各种bug，比如我提交的这个。 里面还有很多的bug以及我不满意的地方（不知道为什么能活到现在……），反正 所以我现在自己写了我自己的版本。 现在的左侧搜索框应该能显示搜索出来的节选高亮了。问题终于解决了（大概

Agolia的我还是先留着吧，毕竟我自己写的也没有特别满意，而且他们也帮我卖广告 了所以就 都保留着想用哪个用哪个吧。。

问题和需求

1. 方便：最好是一个小插件或者一段js就好，我懒得换主题而且换了的新主题就算搜索功能很好 也不一定别的功能很好
2. 能搜索全文
3. 搜索出来的东西能高亮：这个是最重要的feature，也是我到处怎么找开源也找不到的feature。 意思就是你搜索正文中的东西能把match上的文字以及前后文的一小段都显示出来而且高亮match。 我看到的基本要么只显示title，要么只能显示正文节选。
4. 免费开源：这样我自己也能改样式
5. API好用

2019-01-18
Yanxi Chen

Partial Functions

System $T$, $F$ are total languages.

PCF (Programming Language for Computable Functions) (By Gordon Plotkin) - E. col. of partial languages.

Idea: Extending the theory of computability to HIGHER TYPE. Standard computability courses only talk about computation over $\mathbb{N}$, but nothing beyond that.

e.g. $gcd$ is defined by the following (recursive) equations:

We can transcribe the above in a real programming language (ML, Haskell) in an evident way.

We call it “Recursive function” in a typical course - it is using recursion.

Then the next typical topic would be about “stack”.

Recursion has nothing to do with the stack. (One obvious example is flip-flop with two $NOR$ gates.)

Better idea (correct idea): simultaneous equations in the variable gcd. Solve for gcd!

We want: $gcd\ s.t.\ gcd=G(gcd)$ where $G$ is the function of definition my $gcd$. We are looking for a FIXED POINT.

The equations only make sense (solution exists) with computable partial functions.

2018-09-30
Yanxi Chen

Hereditary Termination and Logical Equivalence Recap

Hereditary Termination:

• $HT_{\tau}(e)$ hereditary termination at type $\tau$
• $HT_{nat}(e)$ $iff $$e\mapsto^*z or e\mapsto^*s(e’) such that HT_{nat}(e’) (inductively defined) • HT_{\tau_1\rightarrow\tau_2}(e) iff$$if\ HT_{\tau_1}(e_1)\ then\ HT_{\tau_2}(e(e_1))$ (implication)

Logical Equivalence:

• $e\sim_{nat}e’$ $iff$either $e\mapsto^*n^*\leftarrow e’$ or $e\mapsto^*s(e_1),e’\mapsto^*s(e_1’),e_1\sim_{nat}e_1’$
• $e\sim_{\tau_1\rightarrow\tau_2}e’$ $iff$$if\ e_1\sim_{\tau_1}e_1’\ then\ e(e_1)\sim_{\tau_2}e’(e_1’)$

Some theorem:

• $e:\tau\ implies\ e\sim_{nat} e$
• $e\sim_{\tau}e’$ $iff$ $e\simeq_{\tau}e’$
• $e\sim_{\tau}e\ iff\ HT_{\tau}(e)$

2018-09-09
Yanxi Chen

An example to start off

First we have the following two examples of recursive functions

func toStrings(L: int list) string list =
case l of
[] => []
| x::xs =>
IntToString(x)::toStrings(xs)

func add(l: int list, a: int) int list =
case l of
[] => []
| x::xs => (a+x)::add(xs,a)

We can have a more general function as the following

map: for all a and b, (a->b)->a list -> b list
fun map f l =
case l of
[] => []
| x::xs => f(x)::map[a][b](xs)

It is called polymorphism generality.

To achieve these, we need variables in type: we have the following judgement

$\Delta\vdash\tau\ type$ where $\Delta$ means $t_1\ type,…,t_n\ type$

Take the map function as an example:

It reads as: $(a\rightarrow b)\rightarrow a\ list\rightarrow b\ list$ is a type assuming that $a$ is a type and $b$ is a type.

The inference rule for that

• In Searching Counter Examples for Ramsey Number

2018-07-06
Yanxi Chen

This is a project I did in my undergrad, so I might forget some of the details. Also some of the design choices might seen stupid for now, but I am writing them down anyway just for note-taking. The codes on Github. And here is the presentation we have. I assume the readers of this post have basically knowledge of computer science, like graphs, but not necessarily mathematics (I am really bad at mathematics in fact).

What is Ramsey Number?

According to Wolfram Research, it is to Find the minimum number of guests that must be invited so that at least m will know each other or at least n will not know each other. The solutions are known as Ramsey numbers. To phrase it in Computer Science word, for $R(n,m)$, it is to find a complete graph with minimum vertices such that if we color edges in two colors, there is no monochromatic n-cliques and m-cliques in any edge labelling. A counter example of $R(n,m)$ is basically a graph with a a labeling that contains monochromatic clique(s).

How hard is this? Well we know that $R(3,3)=6$, $R(4,4)=18$, and we don’t know anything above $R(4,4)$. For $R(10,10)$, the current bounds are $798$ to $23556$. In the project, we are to design an algorithm/system that make use of basically endless computing power from both super-computers (XSEDE, CondorHTC), and cloud platforms (AWS) to find the largest counter example of $R(10,10)$.

2018-06-28
Yanxi Chen

Introduction

In CPython, the global interpreter lock, or GIL is a mutex that prevents multiple threads from executing Python bytecodes at once. The lock is necessary mainly because CPython’s memory management is not thread-safe.

A Performance Experiment

0 import time
2 import multiprocessing
3
4 NUM = 10000000
5
6 def count(n):
7    while n > 0:
8    ¦  n -= 1
9
12 start = time.time()
13 t1.start()
14 t2.start()
15 t1.join()
16 t2.join()
18 print time.time() - start
19
20 start = time.time()
21 count(NUM)
22 count(NUM)
23 print "single thread:"
24 print time.time() - start
25
26 p1 = multiprocessing.Process(target=count, args=(NUM,))
27 p2 = multiprocessing.Process(target=count, args=(NUM,))
28 start = time.time()
29 p1.start()
30 p2.start()
31 p1.join()
32 p2.join()
33 print "multi process:"
34 print time.time() - start

Here’s the output: