fu_language

fu_language
├── README.md
├── .git/
├── .gitignore
├── .vscode/
├── tokenizer.c
└── tokenizer.exe

• Let’s Build A Simple Interpreter. Part 1. - Ruslan’s Blog 🔼
• [[]]
  关键字：”;”, “(“, “)”, “[“, “]”, “{“, “}”, “|-“, “-|”, “:”, “:=”, “|”, “,”, “->”, “::”, “_“, “=”, “…”
  优先级：语义符号 (-> , |三者相同) :: : := == (|- -|二者相同) ;
  同一行从右到左

函数式
实际上很接近Agda
部分关键字大写开头以区分

行、块

单个文档，{}中的内容即一个块
块是一个广义上的（希尔伯特式的）推演
每一行组成推演序列，用；分隔），其中最后一行是结论（导出项）
推演序列要求每项必须由公理或之前项推得，由于 一阶逻辑的不可判定性，nontrivial的要显式用|-指定，方便计算机验证。找不到的项自动视为假设
同时块具有命名空间隔离的效果

逻辑真理 ≠ 算法可计算
命名空间(语法上的推导)和’类型空间’不同
比如sum = A + B只能表达出2 * sum之类的, 而无法自动表达2 * A + 2 * B
C := A, B | D;
E := C ]]合法, 命名空间有限, 可以自动传
E := B | D =< C ]]需要额外解释

请注意这里的 := : ]] @都是语法上的符号, 我们用 == 表达这种等式, 比如 a, b ]] == b
例如我们可以在语法上说6/3的除数是3, 但不能说2的除数是3, 6/3和2只是在值上相等, 其实是两个表达式

如果加了export, 才可以通过name.something访问
packet := {n: Nat := 1
export n}//export n == (expr n, 1) 注意这里实际上用了n的名字, 所以是语法上的
a = packet.”n”//_ . _ 是查找函数

//另一个文件
//环境: (“packet”, (“n”, 1)), …
import “packet” form env;
// _ from _ 是另一种查找函数, “packet” form env = “packet”, (“n”, 1)
//这里import将packet加入命名空间, 这里依旧是不能覆盖已有值的
//注意import实际上可以用于假设公理
//import “classic”, ((a -> False)-> False) = a
a = packet.”n”
import “n” form “packet” from env;
//如果在同一个文件, 也可以甚至可以直接import packet, 然后环境中就有n了
b = n
import (“packet” from env) as “p”;//这里的 _ as _ 是替换函数

something
left_rev = right_rev =< {
	a: G; l := left_rev a; r := right_rev a;
	one * e @ ~ => l = l * e;
	rev ]] * @ ~ => ~ = l a r;
	rev [[ * @ ~ => ~ = e r;
	one * e @ ~ => ~ = r;
	by => left_rev = right_rev}

//by 表示逻辑闭包(根据当前块中的命题(变量, 即使没赋值每一行也自动形成一个变量)能推出的所有), 或许可以省略(具体看性能)
//单独的by => 也可以不写

inf_prime := max Prime -> False =< {
	max Prime |- {
		Premise => Q := max Prime;
		something => M := ∏ q <= Q q + 1;
		p: Prime, p <= M -> not p | M => M: Prime;
		False};                
	Goal}
	
//也可以用分析法反着推

从目标反推？在写了 A =< {可以读取Goal}, A |- {可以用Premise}
结构冗余? 用~表示上一个结果 or 等式值，~~表示上两个结果 or 等式值…

不能写{n: Nat; a: Nat := 2 * x; a}因为x没赋值
只能{n: Nat := 1; a: Nat := 2 * x; a}

类型

声明(实例化) a: A 注意声明过后依然是自由变元，除非实例化
赋值 n: Nat := 1
依赖类型语法 a:: A, a是形式参数, 并不会声明a
必须声明类型且不能重复声明

用Type n 表示 Sort n, Type = Type 1，可以

自动提升（也就是所谓的多态）: 自动找始对象或终对象等进行态射
eg.1/2 = 0.5自然数上本来就没定义除法, 1, 2提升到有理数
eg. i/1 = i “/“提升到复数
eg. a: G = a>: Group 集合提升到群，即a: G >:
两个类型不同的对象一般不会被视为相同，即使“内容看起来一样”；而在集合论里，同一个集合元素可以属于多个集合
A in B 在类型论中一般表述为有一个自然含入映射

• 等价即等于? Prop1, Prop2 = Prop1 语法上怎么说更好

和类型、积类型、指数类型

和类型 A | B

积类型a, b或(a, b)
a, b, c = (a, b), c = a, (b, c)
括号只是用来区分优先级, 无实际作用
注意其他地方不要随便打逗号 eg. a b c : G -> a * b * c = a * (b * c)
(a, b) ]] == b, (a, b) [[ == a, (0, 1, 2, 3) [[2]] == 2 这里用的自然数代表将函数作用几次的定义

幂类型A->B
复合(A->B)@(B->C) == (A->C)
恒等函数 _
注意这里[[和]]和@是语法上的函数, 因为a, b实际上=b, a

之所以用符号, | ->是因为构造的是对应类型的对象, 并非同一类型的操作
保留+ * ^用于同一类型

eg. List a = True | a, List a

依赖类型

依赖类型写法同一般的类型，如
F(a: A): phi a 等效于 F: (a:: A -> phi a)
a:: A, phi a

定义类型a:: A, phi a = b:: A, phi b// a，b只是个哑变元(否则不能反复声明类型)
a: A, …: phi a声明变量类型

eg. List a := True | a, List a
Nat := True | Succ Nat
Succ: (Nat -> Nat) 这里是自动转为 Succ Nat = n:: Nat, Succ n
_@_ f: (C <- B) g: (B <- A) = a:: A, b:: B, b = g a, c:: C, c = f b
(C <- B) @ (B <- A) = (C <- A)

a0::, Prod [[ = a0

每个类型可以看作一个关于自身良定义（可居性，存在一个对象）的命题
用Maybe单子修饰一个可能不存在的对象，如
a: Maybe A而不用提供A的良定义证明
因为Maybe A = True | A一定可居( 传统的True = None:: … )

//用“广义和类型”的方法(即n元组), 在lean中用的是类似函数的方法
//不能用函数(广义积类型), 因为只能证明对某个G有定义
monoid := G:: Type u, *:: (G -> G -> G), 1:: G,
	(assoc [*] [G]:= a b c:: G -> a * b * c = a * (b * c)),
	(one [*] [1] [G]:= a:: G -> a * 1 = a);
	
//
	
BinaryMonoid: monoid :=
	G := e | a,
	_ * _:={
	e * := _
	a * a := e},
	pf_mul_assoc:= ...,
	pf_mul_one:=...;

//证明部分还要学习

函数（指数类型）

f(x: ℝ) : ℝ := x + 1; 这相当于一个语法糖, 不会真正声明变量x
//f := {x: ℝ -> x + 1} 括号防止命名空间污染
// f: := _ + 1: ℝ 这里相当于提升了1和+
// f: (ℝ -> ℝ) := _ + 1 这里 _ 的类型其实是 ℝ -> ℝ
_ f' := f;
// x f'
// _ f' x
// _ 表示输入变量且每一个不同 如 _ + _ = add
Do print (f' = f); //>>>True //只是表达方式不同

g x := {y := x ^ 2; 2 y};
g x := {2 y -| y := x ^ 2};
Do print type f;
//>>> ℝ -> ℝ
Do print g 1;
//>>> 2

显式闭包(自由变元)

y[x] = x + 1;
z[y[x]] = y[x] + 1;
Do print y = z //>>>false
x = 1
w = z + 1 //这里的z已经被完全绑定, 所以不用写[x]

func2 (x:: Type u) [x :^ myType] : Type v = ... 

• Group of G引入of
  …自动从环境中找

存在与时间

纯函数只是描述性的，特别的在fu语言中只能描述存在
我们声称一切都是纯函数、无副作用，但最终却需要一个”不纯”的主函数作为程序的入口点。这就像构建了一个完美的数学宇宙，却需要从外部”踢一脚”才能启动。
无穷次才能收敛的递归，实际上存在的编译时间，不可判定，无限运行的主循环

程序不是运行在时间中，而是时间自己在通过程序收敛成为世界（存在）。

～可能世界语义学
Do IO a->World
Be ‘非计算性的存在性命题的单子’计算可能失败（不终止/不可执行）= Possible｜，其中Unknown: Possible
Rand

将单纯的构造性逻辑Decidable 提升到World 或者叫Time 或者叫 Timeline

实现

自定义语言
~meow语言

富文本

代码部分用{}标记, 渲染时用>>>标出部分# 代码结果
外面是[[Vion_editor]]: 采用markdown语法, 可以在一行的开头用# 紧接命令, 也用c风格的注释
右边栏有渲染结果, proof, message 等

misc

广义张量

V  W: VecterSpace, α: (ℝ[], Q: orderedBase V) //ℝ[]用来表示ℝ形式向量空间~多项式
M: V α | α* [:W] [:α]
//这里的默认作用是带缩并的张量积, | 表示不带缩并版本
//[:W] [:α]是[w:W] [a:α]的省略