• Dec 29, 2015

    Combinator "seq"

    Haskell 是一门拥有惰性赋值特性的函数式编程语言，Normal Form是表达惰性求值的重要概念， seq 和 deepseq 用于将表达式求值到不同等级的 Normal Form。

  • Dec 14, 2015

    Haskell List Append Performance

    阅读 Graham Hutton 的书 Programming in Haskell 的 Chapter 13 Reasoning about programs 时，书中分析 reverse 函数的时间复杂度时提到Haskell中列表拼接运算符(++)的时间复杂度是$O(n)$的！

    • 2015-11

  • Nov 12, 2015

    The Yin-Yang puzzle

    所谓的 Yin-Yang puzzle，指的是这样一段Scheme代码：

    (let* ((Yin
         ((lambda (cc) (display #\@) cc) (call/cc (lambda (c) c))))
       (Yang
         ((lambda (cc) (display #\*) cc) (call/cc (lambda (c) c)))) )
    (Yin Yang))

    执行这段代码的输出：

    @*@**@***@****@*****@******@*******@********@********* ...
  • Nov 6, 2015

    自然数的除法与取模

    Coq 对自然数的除法与取模的实现很有讲究！

    皮亚诺公理

    自然数，natural number, 严格定义有皮亚诺公理给出。平亚诺序数理论提出自然数的五条公理，这五条公理的非形式化描述如下：

    1. 0 是自然数；
    2. 每一个确定的自然数 n 都有一个确定的后继，记作 n+1, n+1 也是自然数。
    3. 如果 m，n 都是自然数，并且 m+1=n+1, 那么，m = n。
    4. 0 不是任何自然数的后继。

    5. 如果一些自然数的集合 S 具有性质：

      • 1 在 S 中；
      • 若 n 在 S 中，那么 n+1 也在 S 中。

      那么 S = N。(公理 5 保证了数学归纳法的正确性，因此也被称作归纳法原理。)

    皮亚诺公理的形式化描述：

    • (e in S)
    • (forall a in S)(f(a) in S)
    • (forall b in S)(forall c in S)(f(b) = f(c) -> b = c)
    • (forall a in S)( f(a) /= e)
    • (forall A in S)(((e in A) and (forall a in A)(f(a) in A)) -> (A = S) )

    自然数的运算

    根据自然数的归纳原理，容易给出自然数的加法、减法和乘法运算：

    Fixpoint add (a  b : nat) : nat :=
  match b with
    | O    => a
    | S b' => addition (S a) b'
  end.

Fixpoint subtract (a b : nat) : nat :=
  match a, b with
    | _, O => a
    | O, _ => O
    | S a', S b' => subtract a' b'
  end.

Fixpoint multiply (a b : nat) : nat :=
  match b with
    | O => O
    | S b' => add a (multiply a b')
  end.

    而除法和取模的运算具有很强的技巧性：

    Fixpoint nat_divmod (a b quotient remainder : nat) : nat * nat :=
  match a with
    | O   => (quotient, remainder)
    | S t =>
      match remainder with
        | O   => nat_divmod t b (S quotient) b
        | S r => nat_divmod t b quotient r
      end
  end.

Definition nat_div (a b : nat) : nat :=
  match b with
    | O   => b
    | S t => fst (nat_divmod a t 0 t)
  end.

Definition nat_mod (a b : nat) : nat :=
  match b with
    | O   => b
    | S t => t - snd (nat_divmod a t 0 t)
  end.

    • 2015-10

  • Oct 25, 2015

    Church Encoding

    丘奇编码是把数据和运算符都嵌入到 lambda 演算中的一种方式，整数、布尔值、序对、列表等都可以映射到使用丘奇编码的高阶函数中。

  • Oct 23, 2015

    Web Messaging 以及 jschannel.js 用于页面间跨域通信

    Web Messaging (Cross-document Messaging) 技术是 HTML5 规范中定义的允许不同源站点的页面进行通信的应用程序接口。可以有效地解决在 同源策略的限制下不同站点的页面不能有数据交互的问题。

  • Oct 4, 2015

    使用 VS2015 编译 Cython 程序

    Cython, C-Extensions for Python, 通过 Cython，可以把 Python代码编译到 C 语言代码，甚至在 Python 代码中混用 C 语言的 native 数据类型， 进一步编译成动态链接库，从而极大地提升程序的运行效率。

  • Oct 4, 2015

    《Purely Functional Data Structures》笔记

    Purely Functional Data Structures. Chris Okasaki. September 1996. CMU-CS-96-177. School of Computer Science. Carnegie Mellon University. Download pdf version from CMU. 与此相关的 StackExchange 上的另一个问题：What’s new in purely functional structures since okasaki ?。

    C语言程序员学习数据结构往往很容易找到很多优秀的教科书，但是，诸如使用 Standard ML 和 Haskell 的函数式编程语言程序员去很难拥有这种奢侈品。尽管有一些为命令式语言设计的 数据结构很容易用函数式编程语言实现，但是，most cannot，原因在于函数式编程语言并不赞成使用这些数据结构所依赖的那种赋值方式。这本书将展示延迟求值(lazy evaluation) 在 amortized functional data structure 中的基础性的作用，以及与可持久化(presistance)数据结构的联系，还有将 strict 和 lazy 两种求值策略组合在一起，以及 polymorphic recursion, higher-order 和 recursive modules.

  • Oct 2, 2015

    static_assert

    assert 是 C/C++ 中的运行时断言机制，但是，如果包含断言的函数不被调用，就无法触发该断言， 实际上，编译期的断言也非常重要，例如在模板实例化时的编译期断言很有利于提高程序的质量。Boost 库中内置了 BOOST_STATIC_ASSERT 断言机制，C++0x/C++11标准中也加入了 static_assert 断言。不借助 Boost 库和 C++0x/C++11，如何实现一个编译期断言？

    • 利用 switch...case 语句中两个 case expression 不能相等的机制
    #define assert_static(e) \
    do { \
        switch (e) case 0: case(e): ; \
    } while (0)

    使用 do {} while (0) 可以使得 assert_static 宏在使用的时候更像是函数调用。这一技巧在 Linux 内核中的队列实现部分也有很多非常精彩的运用。

    • 利用数组长度不能为负数的机制
    #define assert_static(e) \
    do { \
        int __assert_static[(e) ? 1 : (-1)]; \
    } while (0)

    这么使用 do {} while (0) 可以将数组定义包裹在一个新的作用域中，不至于引起和程序中已经定义 的变量的冲突。

    值得一提的是，深入理解 C++11 新特性解析与应用 一书中第30页使用了 “‘除0’会导致编译器报错” 来实现 assert_static 的方法是不正确的。在 C++ 中，“除0” 是未定义行为，在 C++11 标准 (ISO/IEC14882) Section 5.6 中，明确指出

    If the second operand of / or % is zero the behavior is undefined.

    至于为什么要这么做，C++ 之父 Bjarne Stroustrup 的 The Design and Evolution of C++ (Addison Wesley, 1994) 一书中提到

    low-level events, such as arithmetic overflows and divide by zero, are assumed to be handled by a dedicated lower-level mechanism rather than by exceptions. This enables C++ to match the behaviour of other languages when it comes to arithmetic. It also avoids the problems that occur on heavily pipelined architectures where events such as divide by zero are asynchronous.

    • 2015-09

  • Sep 18, 2015

    钱币兑换问题

    钱币兑换问题：

    仅有 n 种指定面值的硬币(c1, c2, c3, …, cn), 将钱 N 兑换成 这些面值的硬币，总共有多少种兑换方法？

Subscribe via RSS

← Newer
Older →