-
C++模板的图灵完备
一门编程语言图灵完备，指的是能够计算任何一个图灵可计算的函数，或者说，可以用来模拟通用图灵机。
-
Pell's Equation
Pell’s Equation值得是形如 \(x^2-Dy^2=1\) 的一类丢番图方程(Diophantine Equation)，其中，$D$是一个正的非完全平方数。
-
Haskell中FFI的使用
FFI, Foreign Function Interface, 用于在一种编程语言调用另一种编程语言编写的函数。Haskell的FFI提供了 Haskell编写的程序调用其它语言编写的函数或者在其他语言中调用Haskell的函数，以进行协作的能力。
-
Python的类型标注与检查
Python作为一个动态类型语言，支持Subtyping和Duck Typing，一些Lint工具可以对Python代码静态进行类型 检查来提高程序质量，还有工具可以支持类型标注和检查，并编译代码以提升性能。Python 3.5又引入了 Type Hints机制来提供统一的类型标注协议。
-
Monad 与 Continuation
Continuation 是一个非常重要的概念，用于表达程序执行过程中某一处的上下文。处于会破坏引用透明的原因，Haskell中并没有像Scheme那样在语言 级别提供对Continuation的支持，Continuation是一个Monad类型，而另一方面，Continuation可以被用来实现各种Monad。
-
Arithmetic on Types
Haskell’s algebraic data types are named such since they correspond to an initial algebra in category theory, giving us some laws, some operations and some symbols to manipulate. – by Don Stewart, answer for the question Haskell’s algebraic data types.
-
Notes on Combinatory Logic
Combinatory logic is a way which eliminates the need for quantified variables in lambda calculi. It was introduced by Moses Schonfinkel and haskell B. Curry, and has been used to as the basis for the design of functional programming languages, such as Haskell.
-
Concept in C++
Concept is a term that describes a named set of requirements for a type.
-
A Formal Proof for Square Root of 2 is Irrational
It was one of the most surprising discovers of the Pythagorean, a famous Greek mathematicians, that there are irrational numbers. The square root of $2$ sometimes has the name Pythagora’s Constant:
\[\sqrt{2} = 1.4142135...\] -
使用generalize的技巧
Coq中
generalize和generalize dependent的用法说明如下：generalize term: This tactic applies to any goal. It generalizes the conclusion with respect to some term.generalize dependent term: This generalizes term but also all hypotheses that depend on term. It clears the generalized hypotheses.
2016-05
2016-04
2016-03
Subscribe via RSS