Maths (or PL) Related Stuff

‘24

May 10

prism.js 没有 Lean 的语法高亮，且用 Coq 替代。

1

Given a group which satisfies mul_assoc one_mul mul_left_inv where
Proof that 1.

想法是后两个定理比较简单，而命题左侧应该可以化成由这两个定理组成的式子。最后无论如何应该是用定理 (3) 才能证到，但因现在不是阿贝尔群，不满足交换律，所以 (3) 中的肯定是一个含有的整体。

那也没什么想法，反正先化，走一步看一步：

我们整出来了这项；注意划线部分，现在比较明朗了：

或者用Lean:


theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
  calc 
    a * a⁻¹ = (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) := by
      nth_rw 1[<-one_mul a]
      rw[mul_assoc]
      rw[<-mul_left_inv (a * a⁻¹)]
      rw[mul_assoc]
    _ = 1 := by
      rw[mul_assoc,<-mul_assoc a⁻¹,mul_left_inv,one_mul]
      rw[mul_left_inv]

这个题是我在学习Lean的时候碰到的。他给的解答注意力比较集中，我比较蠢笨想不到，就记录了自己的做法。

证出来上面这个，后面两题就简单了。最后一题其实证明并不复杂，但是我为了能用 have （所以说我就不喜欢「注意到」）辅助定理的写法和 apply exact 只好写的比较长了。


theorem mul_one (a : G) : a * 1 = a := by
  rw[<-mul_left_inv a,<-mul_assoc]
  rw[mul_right_inv]
  rw[one_mul]

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  have
    H: b⁻¹ * a⁻¹ * (a * b) * (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
      nth_rw 2[<-mul_one (b⁻¹ * a⁻¹)]
      rw[<-mul_right_inv (a * b)]
      nth_rw 2[mul_assoc b⁻¹]
      rw[<-mul_assoc a⁻¹ (a * b),<-mul_assoc b⁻¹,<-mul_assoc b⁻¹]
  rw[mul_assoc b⁻¹ a⁻¹,<-mul_assoc a⁻¹,mul_left_inv,one_mul,mul_left_inv] at H
  rw[one_mul] at H
  apply H

2 Church Encoding

首先定义一个记号：

记号表示函数应用次（自己复合次）。Church 编码用这个复合的函数表示数，且函数复合的次数就是数的值。当时觉得这个定义特别怪。现在在学类型论来看是有些明白了：

考虑一个自然数类的递归定义 (Inductive Type):


inductive ℕ where
  | zero: ℕ
  | succ: ℕ -> ℕ

that is

zero succ 都是类型构造子，这时候譬如就可以写成

正好，这里就应用了 3 次。我想 Church 的定义肯定就是如此归纳出来的。不过之前我连 successor function 都不知道，更多的应是自己学艺不精了。

May 14

on composition notation

之前洗澡的时候想过一个问题：莱布尼兹的引进的记号中的是一个右结合的算符（姑且这样说）。但大部分书写系统都是从左到右，包括 Leibniz 自己的语言。这样函数复合的时候就比较头痛：一般不会从左往右写，而是先写内层函数，然后再回过头来在左侧写外层函数，因为这很 intuitive：符合计算顺序。

当然 Leibniz 本人并未考虑这么多，且数学中函数通常一两个字母或符号，并不麻烦写——而且之后有了，但到了 PL 这儿就不一样了：函数名可以很长。如果进行复合操作就需要经常左右横跳光标——考虑下面这个函数：


(some-very-long-and-verbatim-function x y z)
;~~~~~~~~ where cursor at~~~~~~~~~~~~~~~~~~~^
; we want to pipe the result into some other function:
(some-other-function (some-very-long-and-verbatim-function x y z)
;^
(some-other-function (some-very-long-and-verbatim-function x y z))
;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^

Lisp 很好，包括 Sexp 大多数时候比 Infix 要好的。但唯独复合不好——因为 (f x) 和 f(x) 实质上没太大区别，复合需在左侧补函数名和左括号，右侧补参数和右括号。同时其更不具备一般语言具有的 method chaining，难上加难。

上例若用 Vim, 输入序列就是


; inoremap jk <ESC>
I(some-other-function<space>jkA)

~~ur cringe for not using vim~~

相当之繁琐（前提是该行只有此函数，否则更繁）且不是很 Intuitive. 我喜欢 Intuitive. 注意到上面我用了 Pipe 这个词，说明复合其实和管道操作类似，所以 ES6 的提案里边引入了 |> 算符，和 shell 的管道是一样的。写代码时我经常想念管道。

proposal-pipeline-operator

tc39 • Updated Sep 11, 2024

那实际上这个是和 Elixir 学的：


"hello, world!"
|> String.split(" ")
|> Enum.map(&String.capitalize/1)
|> Enum.join

或者像 Haskell 和一众受了其影响的一样：用 . 表示复合，和数学类似。这功能亦可用 Lisp 实现，重载 . 这个原本用于 cons 的 reader macro character.

当然 Haskell 也有 |> （虽然我写的是 Lean）：


def sigma (l : Nat) (r : Nat) (f : Nat -> Nat): Nat :=
  List.range (r - l + 1)
  |> .map (λ n => f (l + n))
  |> List.foldl (· + ·) 0

#eval sigma 1 10 id -- => 55

当时在澡堂里搓身子的我就想到：为何不用来表示复合呢？这是很自然的想法。这样从左往右读，直接计算每一步是很直观的，当然需要指出此处函数符号是左结合。当时觉得自己的想法颇 primitive，但无独有偶，群论里确有这样的记法，正好和我的想法一致——看来这样的想法是自然的。

由此就想到后缀记法，感觉上面的记法和后缀记法是相仿的。

Coalton 不错， compose 和 pipe 都有实现。


(coalton-toplevel
    (declare add (Integer -> Integer -> Integer))
    (define (add x) (fn (y) (+ x y)))
    (declare mul (Integer -> Integer -> Integer))
    (define (mul x) (fn (y) (* x y))))

(coalton (progn
          ; => ((add 3) . (mul 2)) 2
          ((compose (add 3) (mul 2)) 2)
          ; => ((add 3) . (mul 2)) 2
          (nest (add 3) (mul 2) 2)
          ; => 2 (mul 2) (add 3)
          (pipe 2 (mul 2) (add 3))))

(+ Lisp Haskell) ⇒ Coalton


sigma =: 1 : '+/@:u@(i.@>:@-~)'