Mingjian's Blog

好记性不如烂笔头, 何况烂记性.
人生如不能回档的游戏, 保持升级直到角色死亡.

LeaderF现在基本是Vim最好的模糊查找插件. 其基本功能和演示可以参考作者Yggdroot的几篇文章介绍:

本文是用来记录个人对工具的理解和学习过程. 记录各种应用场景里如何使用LeaderF, 如何配置.

什么是模糊查找

模糊查找的应用场景特别常见. 就是在海量信息中查找你想要的信息.

阅读全文 »

由于一个工作需要把大量的vbscript脚本转换成python脚本, 需要学习一下python的ast模块, 本文是一些干货的笔记. 由于当前最新的python 3.8的官方文档过于简略, 主要参考和翻译绿树蛇的文档和python3.10pre的文档.

AST是Abstract Syntax Trees的缩写, 中文是抽象语法树.

AST和code的转换

python代码有三个分身,

  1. 以unicode字符串存在的源代码. 人类可读写, python解释器不可读.
  2. 以AST对象存在的抽象语法树. 人类可读写, 但很难读懂原来的语义, 用来显示python语义元素之间的关系. 是从源代码翻译成目标代码的中间产品.
  3. 以code object存在的可执行的目标代码. python解释器可读, 人类不可读.
阅读全文 »

\(\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\DEF{\sf{D\scriptsize EF}.\quad}\) \(\def\DEFi{\sf{D\scriptsize EF}^*.\quad}\) \(\def\DEFn{\sf{D\scriptsize EF}_*.\quad}\) \(\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}\) \(\def\llbracket{\unicode{x27E6}}\) \(\def\rrbracket{\unicode{x27E7}}\) \(\def\PROOF{\sf{P\scriptsize ROOF}.\quad}\)

点击这里进入AMIL目录

Problem 1

Show that (a) \(\Gamma;\alpha\vDash\varphi\) iff \(\Gamma\vDash(\alpha\rightarrow\varphi)\); and (b) \(\varphi\tauequ\psi\) iff \(\vDash(\varphi\leftrightarrow\psi)\).

\(\PROOF\)

阅读全文 »

\(\def\PROOF{\sf{P\scriptsize ROOF}.\quad}\)

点击这里进入AMIL目录

Problem 2

Show that no one of the following sentences is logically implied by the other two. (This is done by giving a structure in which the sentence in question is false, while the other two are true.)

  1. \(\forall{x}\forall{y}\forall{z}(Pxy\rightarrow Pyz\rightarrow Pxz).\) Recall that by our convention \(\alpha\rightarrow\beta\rightarrow\gamma\) is \(\alpha\rightarrow(\beta\rightarrow\gamma).\)
  2. \(\forall{x}\forall{y}(Pxy\rightarrow Pyx\rightarrow x=y).\)
  3. \(\forall{x}\exists{y}Pxy\rightarrow\exists{y}\forall{x}Pxy.\)
阅读全文 »

\(\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\DEF{\sf{D\scriptsize EF}.\quad}\) \(\def\DEFi{\sf{D\scriptsize EF}^*.\quad}\) \(\def\DEFn{\sf{D\scriptsize EF}_*.\quad}\) \(\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}\) \(\def\MYNOTE{\sf{M\scriptsize{Y}}\sf{N\scriptsize{OTE}}.\quad}\)

这是一个关于数理逻辑的读书笔记或者学习总结, 书名是A Mathematical Introduction to Logic, 作者Herbert B. Enderton, University of California

本文是Chapter 0, 点击这里进入目录

第0章介绍一些集合论的基础概念, 这些概念是后面所有章节的基石. 我基本是把干货抄录在这里以便跳转

阅读全文 »

这里记录一些听到或看到的我认同的别人的观点. 好记性不如烂笔头, 自己说不明白就记录一些别人说的金句. 将来孩子长大了, 要离家了, 如果我的观点还没变, 拿给孩子看看. 虽然不一定有用\(\unicode{x1F602}\), 毕竟年轻人很少听老人言.

阅读全文 »
0%