GaeBlogX Software Development [email protected]@Irvine

2019-01-20
Yanxi Chen

# Recap for Product/Sum Types

Brief recap for product and sum to have a consensus on notations.

## Product Types

$\tau_1\times\tau_2$

### Introductions

$\frac{\Gamma\vdash e_1:\tau_2,\Gamma\vdash e_2:\tau_2}{\Gamma\vdash <e_1,e_2>:\tau_1\times\tau_2}$

### Eliminations

$\frac{\Gamma\vdash e:\tau_1\times\tau_2}{\Gamma\vdash fst(e):\tau_1}$ $\frac{\Gamma\vdash e:\tau_1\times\tau_2}{\Gamma\vdash snd(e):\tau_2}$

## Sum Types

$\tau_1+\tau_2$

### Introduction

$\frac{\Gamma\vdash e_1:\tau_1}{\Gamma\vdash inl_{\tau_1,\tau_2}(e_1):\tau_1+\tau_2}$ $\frac{\Gamma\vdash e_2:\tau_2}{\Gamma\vdash inr_{\tau_1,\tau_2}(e_2):\tau_1+\tau_2}$

### Eliminations

$\frac{\Gamma\vdash e:\tau_1+\tau_2;\Gamma,x_1:\tau_2\vdash e_1:\sigma;\Gamma,x_2:\tau_2\vdash e_2:\sigma}{\Gamma\vdash case(e)of\{inl(x_1)\hookrightarrow e_1,inr(x_2)\hookrightarrow e_2\}:\sigma}$

## Unit

$\frac{}{\Gamma\vdash <>:unit}$

• # 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:

$gcd(m,n) = m\ if\ m=n\\ gcd(m,n) = gcd(m-n,n)\ if\ m>n\\ gcd(m,n) = gcd(m,n-m) ow$

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:

$a\ type,b\ type\vdash(a\rightarrow b)\rightarrow a\ list\rightarrow b\ list\ type$

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

$\frac{\Delta\vdash\tau\ type;\Delta\vdash\sigma\ type}{\Delta\vdash\tau\rightarrow\sigma\ type}$ $\frac{\Delta,t\ type\vdash\tau\ type}{\Delta\vdash\forall\ t.\tau\ type}$

• # 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)$.

Search
Categories