GaeBlogX Arista Networks, Software-Defined Networking

• # 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
[] => []


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)
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:

multithread:
1.70929884911