函数式编程是不是在形式逻辑上走的太远了？

[none_nobody]

刚到手了几本大部头的统计学习的纸书，顺势想起另一个方向上函数式编程是不是走的太远了，

在实际开发中，函数式编程解决了什么样的问题（除了一次元的），形式逻辑的运算在函数式编程多用的么？

或者二次元的运算符能计算了么？比如 haskell 里除了
higher order functions, lazy evaluation, static polymorphic typing, user-defined datatypes, （窃以为这是一次元函数式）

后面的这两种 pattern matching,  list comprehensions. （二次元函数式）函数式编程的程序能够进行自我构建定义不？

用函数式编程开发过大项目的出来说说。

[Zoom.Quiet]

关注 伞哥 的weibo 就知道了,
因为 FP 发展成熟的比较早,
所以,有很多商用/军用的大型系统,一直运维/销售到现在;
只是因为都非常昂贵以及关键,处以,基本没有怎么宣传;
不象其它语言,不宣传就没有人用了,,,所以,,,

> --
> -- You received this message because you are subscribed to the Google Groups
> Shanghai Linux User Group group. To post to this group, send email to
> sh...@googlegroups.com. To unsubscribe from this group, send email to
> shlug+un...@googlegroups.com. For more options, visit this group at
> https://groups.google.com/d/forum/shlug?hl=zh-CN
> ---
> 您收到此邮件是因为您订阅了 Google 网上论坛的“Shanghai Linux User Group”论坛。
> 要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 shlug+un...@googlegroups.com。
> 要查看更多选项，请访问 https://groups.google.com/groups/opt_out。



--
人生苦短, Pythonic! 冗余不做,日子甭过!备份不做,十恶不赦!
KM keep growing environment culture which promoting organization be learnning!
俺: http://about.me/zoom.quiet
许: http://creativecommons.org/licenses/by-sa/2.5/cn/

[Chaos Eternal]

给个地址啊楼上


2013/9/17 Zoom.Quiet <zoom....@gmail.com>:

[liyaoshi]

linux kernel ?

还有就是，STM32  V850 RL78

内存小于4k的系统，你们玩过么？

[Chaos Eternal]

玩过啊，最早玩的机器就是这么大的内存好像

可以说forth?

2013/9/17 liyaoshi <liya...@gmail.com>:

[none_nobody]

歪楼了吧。8051 和 z80 好像都至少64K， 4K 内存的高级货，不记得玩过。

回到形式逻辑。

有自构建形式逻辑的开发系统么？

On Tuesday, September 17, 2013 8:52:33 AM UTC+8, liyaoshi wrote:

[Grissiom]

2013/9/17 none_nobody <lyx...@gmail.com>

歪楼了吧。8051 和 z80 好像都至少64K， 4K 内存的高级货，不记得玩过。

51 只不过是最大 64K 的地址空间。现实中 1K 的内存都已经很大了。

 

回到形式逻辑。

有自构建形式逻辑的开发系统么？

On Tuesday, September 17, 2013 8:52:33 AM UTC+8, liyaoshi wrote:

--
-- You received this message because you are subscribed to the Google Groups Shanghai Linux User Group group. To post to this group, send email to sh...@googlegroups.com. To unsubscribe from this group, send email to shlug+un...@googlegroups.com. For more options, visit this group at https://groups.google.com/d/forum/shlug?hl=zh-CN
---
您收到此邮件是因为您订阅了 Google 网上论坛的“Shanghai Linux User Group”论坛。
要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 shlug+un...@googlegroups.com。
要查看更多选项，请访问 https://groups.google.com/groups/opt_out。

--
Cheers,
Grissiom

[Chaos Eternal]

先题外话：窃以为haskell的函数式太纯粹了。

然后不太明白你说的自我构建是什么意思，如果你是说first-class-function，那是所有的函数式都有的，类似的还有 currying 这些。
然后函数就可以返回一个函数然后再返回一个函数去计算你要的东西，当然闭包特性在这里起了很大的作用。

偶到没有开发过大项目，不过之前搞guile-scsh, 现在在搞guile-termite, 把erlang otp的一些特性移植到guile上。
这里夸两句scheme:
1. s-表达式的强大就不用说了，对括号有障碍的可以考虑用emacs+unparenmode、rainbow-parenmode配合上paredit可以基本上消除数括号的痛苦了；
2. 不是纯函数，对副作用不像haskell那样原教旨式的排斥，所以更灵活，而像haskell里面那种为了保持执行顺序的monad在scheme里面也可以用call/cc以及delimited-continuation来实现（monad跟cps是可以互相转换的），因此你如果要做纯函数也可以；
3. 闭包特性，lexical-scope,
这一点比common-lisp要干净点，因为common-lisp实际上是几种老lisp的融合，老的dynamic-scoping没除的太干净；
4. 按需进行惰性求值；
5. 弱类型检查，这个我到不觉得就有多好，不过也不坏；
6. hygienic-macro支持，最近在微博上高端大气上档次的DSL就是从这里开始的，scsh和termite里面都有不少这样的东西；

然后夸两句guile:
1. GNU的scheme实现, r6rs兼容， srfi也支持得不少
2. threading支持（话说posix类系统上做threading真痛苦)
3. 强大的自定义reader, 可以开发多种sub language, 可以跑 bfl, lua, javascript,
有人在做python的，还有个哥们在做prolog
4. 开发比较活跃，最近在做的2.2版本要搞RTL神马的，promise 性能会上台阶
5. 有个叫artanis的web framework


然后说一下zq说的贵的问题：
scheme界有个神一样的存在，chez scheme, 号称跟C跑的一样快，但是没有source, 卖的还停贵的，显然有人买帳嘛。
chez多快不知道， chez有个免费的解释执行版本，据说跑得已经比guile快很多了，然后chez作者的学生写了个ikarus,
经我实测确实很快（算fib比C慢30%,
而其他的scheme比C慢一个数量级），然后ikarus那哥们不做了，有人fork了个vicare出来，也挺快的。
话说，如果scheme能跟C做到类似的速度，谁还要用C++?!

2013/9/17 none_nobody <lyx...@gmail.com>:

[Chaos Eternal]

不知道你要prolog呢，还是ACL2..哈哈

2013/9/17 none_nobody <lyx...@gmail.com>:

[Grissiom]

2013/9/17 Chaos Eternal <chaose...@shlug.org>

先题外话：窃以为haskell的函数式太纯粹了。

然后不太明白你说的自我构建是什么意思，如果你是说first-class-function，那是所有的函数式都有的，类似的还有 currying 这些。
然后函数就可以返回一个函数然后再返回一个函数去计算你要的东西，当然闭包特性在这里起了很大的作用。

偶到没有开发过大项目，不过之前搞guile-scsh, 现在在搞guile-termite, 把erlang otp的一些特性移植到guile上。
这里夸两句scheme:
1. s-表达式的强大就不用说了，对括号有障碍的可以考虑用emacs+unparenmode、rainbow-parenmode配合上paredit可以基本上消除数括号的痛苦了；
2. 不是纯函数，对副作用不像haskell那样原教旨式的排斥，所以更灵活，而像haskell里面那种为了保持执行顺序的monad在scheme里面也可以用call/cc以及delimited-continuation来实现（monad跟cps是可以互相转换的），因此你如果要做纯函数也可以；
3. 闭包特性，lexical-scope,
这一点比common-lisp要干净点，因为common-lisp实际上是几种老lisp的融合，老的dynamic-scoping没除的太干净；
4. 按需进行惰性求值；
5. 弱类型检查，这个我到不觉得就有多好，不过也不坏；
6. hygienic-macro支持，最近在微博上高端大气上档次的DSL就是从这里开始的，scsh和termite里面都有不少这样的东西；

然后夸两句guile:
1. GNU的scheme实现, r6rs兼容， srfi也支持得不少
2. threading支持（话说posix类系统上做threading真痛苦)
3. 强大的自定义reader, 可以开发多种sub language, 可以跑 bfl, lua, javascript,
有人在做python的，还有个哥们在做prolog
4. 开发比较活跃，最近在做的2.2版本要搞RTL神马的，promise 性能会上台阶
5. 有个叫artanis的web framework

这么多优点好心动……

话说 Racket 怎么样呢？嘿嘿嘿……

--
Cheers,
Grissiom

[Chaos Eternal]

freenode上， #scheme 184人， #racket 111人， #guile 58人

2013/9/17 Grissiom <chaos....@gmail.com>:

[none_nobody]

先说，形式逻辑，基本语意定义上有概念、定义、判读、推论、演绎，推理（走的太远了）

自我构建是说，在给定（限定范畴）概念、定义、判断、推论的前提下，运行中形成模式化演绎或则归纳的结构，而无需人工编码。

如上述运行中形成.....人工编码不能实现。

则在函数式编程中，归纳和推理是如何做的，包括
基本逻辑 ： 同一、不矛盾、排中、充足理由。

举例：一种定义  Add ( +  int, int)  可以视为形式逻辑定义了一种概念  UserDefined_Oper ( "oper_character" ,  ”type", "type" )， 同一概念是指：视 UserDefined_Oper 为 A ,  A->A,  这种  [ UserDefined_Oper ] 不可变，

粗略地说，是在 L2 上 UserDefined_Oper 去多态性。

在归纳演绎时，有如下过程 ： 概念（定义）得到  推论。

我的问题在指这里如何定义这个归纳演绎的这个过程，或者程序运行中自动能构成归纳（自构建）
相应的还有类比推理、假设推理等。

上述的在这里可以类比于图结构学习中，在运行中调整节点和边的联系，形成的形式归纳。

[liyaoshi]

虽然不知道你在说什么，但是听上去好像很高级的样子

只是，作为bsp开发人员，我表示oob就是个扯淡

--

[liyaoshi]

OOB的原则就是，造点框，框死你们

OOB的坏处是遏制了创造力

本铞丝的一贯原则是不折腾我会死的

还有，我有心理洁癖

[liyaoshi]

一个事情如果能用1+1的办法解决，干嘛 还要用3-1呢

格物至知的最后目的，只要通原理，就能随心所欲。

[none_nobody]

行，我有点脑裂证。oob 说的是什么？表示不懂。

[none_nobody]

传输带外数据(Out of Band, OOB)？

据说可以有办法让将丢包数据用差分的方法恢复出来，做到即使高铁中也可以不丢包。

[liyaoshi]

Object Oriented Programming

我打酱油跑错地方了？

[liyaoshi]

哦，原来是我拼错了，完了，暴露智商了，你们以后可以忽略我了

[liyaoshi]

或者，你们假装我是中东人

[none_nobody]

继续忽悠二次元开发。

一般我们都是写程序，程序逻辑都是自己写的：

比如这样的程序，是自己构建逻辑的，全扫么。

#include<iostream>
#include<cstdio>

using namespace std;

#define N 4

#define LOOP(i) for(i=0; i<N; i++)

#define F(i) ( (int(*)(int,int))opt[i] )
#define FI F(i)
#define FJ F(j)
#define FK F(k)


int add(int a, int b) { return a + b; }

int sub(int a, int b) { return a - b; }

int mul(int a, int b) { return a * b; }

int div(int a, int b) {
    if (b == 0 || a % b)
        return 2401;
    return a / b;
}

char whichOpt(int index)
{
    if (index == 0) return '+';
    else if (index == 1) return '-';
    else if (index == 2) return '*';
    return '/';
}

void howObtain24(int num[], void *opt[])
{
    int i, j, k, a, b, c, d;
    int ans=0;
    LOOP(i) LOOP(j) LOOP(k)
         LOOP(a) LOOP(b) LOOP(c) LOOP(d)
    {
        if (a == b || a == c || a == d || b == c || b == d || c == d)
            continue;
        if (FI(FJ(FK(num[a], num[b]), num[c]), num[d]) == 24) {
            std::cout << "((" << num[a] << whichOpt(k) << num[b] << ')'
                 << whichOpt(j) << num[c] << ')' << whichOpt(i) << num[d] << endl;
            ans++;
            continue;
        }
        if (FI(FJ(num[a], num[b]), FK(num[c], num[d])) == 24) {
            std::cout << '(' << num[a] << whichOpt(j) << num[b] << ')'
                 << whichOpt(i) << '(' << num[c] << whichOpt(k) << num[d] << ')' << endl;
            ans++;
            continue;
        }
    }
    if(ans==0)
    std::cout << "Non-Answer" << std::endl;
    return;

}

如果是，以随机选择，构建一个大的矩阵，其中含数字 4 牌数列形成一个高级的结构体。

或者更高级一点，程序能够形成乘法口诀里的 2x12 3x8  4x6  的程序逻辑。

[Chaos Eternal]

我倒是有本书，叫 《程序设计语言的形式语义》， 不过还没啃完。

http://www.amazon.cn/%E7%A8%8B%E5%BA%8F%E8%AE%BE%E8%AE%A1%E8%AF%AD%E8%A8%80%E7%9A%84%E5%BD%A2%E5%BC%8F%E8%AF%AD%E4%B9%89-Glynn-Winskel/dp/B0011AN65Y/ref=sr_1_1?ie=UTF8&qid=1379397127&sr=8-1&keywords=%E7%A8%8B%E5%BA%8F%E8%AE%BE%E8%AE%A1%E8%AF%AD%E8%A8%80%E7%9A%84%E5%BD%A2%E5%BC%8F%E8%AF%AD%E4%B9%89

将这个问题讲的比较深入。你要来拿。

然后关于谓词逻辑的语言，真心推荐prolog, 当然根据前文，用scheme也能实现prolog能实现的。
还有ACL2 (A Computational Logic for Applicative Common Lisp) is a
software system consisting of a programming language, an extensible
theory in a first-order logic, and a mechanicaltheorem prover.

我最近到确实在考虑对写的代码做形式证明的事情：
比如对于函数 f :N -> N （考虑到大部分的程序其实都是做这事的，我就简化一下）
用归纳法， 先证明f(1) 成立，然后证明若 f(k)成立则f(k+1)也成立，
后面这个就需要对f(k+1)进行形式转换，然后演绎证明了。
当然这涉及到高阶函数啊，alpha,beta, gamma变换啊等等，所以只是个想法，哈哈。
还是那句话，一起玩啊




2013/9/17 none_nobody <lyx...@gmail.com>:

[none_nobody]

void *opt[N] = { (void *)add, (void *)sub, (void *)mul, (void *)div };

On Tuesday, September 17, 2013 2:03:52 PM UTC+8, none_nobody wrote:

继续忽悠二次元开发。

一般我们都是写程序，程序逻辑都是自己写的：

比如这样的程序，是自己构建逻辑的，全扫么。

在函数式编程中，基础的概念中这些词：

Immutability

Functions as First Class Types

Being able to compose functions.

Monads

Lazy Evaluation & Recursion

S-Expressions

感觉这就是要自构建了，但我又确实不知道怎么能做到。

[Chaos Eternal]

24点我没啥研究，不过shell同学写过，我就搬个link过来：
https://gitcafe.com/shell909090/performance/blob/master/24point/24point-racket.scm

[liyaoshi]

有规则的游戏可以按照规则定义动作

没有规则的呢？

我讨厌条条框框

2013/9/17 Chaos Eternal <chaose...@shlug.org>

[Yiling Cao]

大一下学期，学校教的就是haskell，学的不错，但实际没啥用，比c慢个100-1000倍吧，开拓下思维吧。

[Chaos Eternal]

那是因为编译器没做好。。。

[Chaos Eternal]

On Tue, Sep 17, 2013 at 2:42 PM, Yiling Cao <yilin...@gmail.com> wrote:

> 大一下学期，学校教的就是haskell，学的不错，但实际没啥用，比c慢个100-1000倍吧，开拓下思维吧。
>
>

无责任看了一下， freenode上#haskell有1077人

[Chaos Eternal]

我穿越过那么多位面，还没有见过没有规则的世界。哈哈哈哈。

比如，ZFC集合论总得支持吧，皮阿诺系统总得有吧，1+1总得是1的后继吧，2+3总得是3的后继的后继吧，这不就是规则么？

没有边界条件你怎么解偏微分方程啊，霍金都搞过这个：以没有边界条件这个边界条件解一个模型宇宙。

然后物理上的，在地面上你跳起来总要落下吧，不考虑空气阻力你下落的加速度是个常数吧，考虑空气阻力你有个收尾速度吧，能量要守恒吧，动量要守恒吧，封闭系统的熵总要增加吧，量子去相干就意味着信息的耗散啊。

然后有个叫markov的家伙证明只要有四维以上流型就是图灵完全的，就可以把你放进去然后写出上面的那些邮件！

嘿嘿，纯yy, 莫在意。

[david pu]

+1

2013/9/17 liyaoshi <liya...@gmail.com>

--
 ()   ASCII Ribbon Campaign
 /\   Keep it simple!

[none_nobody]

下单一本；看看。

On Tuesday, September 17, 2013 2:05:55 PM UTC+8, Soahc Lanrete wrote:

我倒是有本书，叫 《程序设计语言的形式语义》， 不过还没啃完。

[Yongwei Wu]

2013/9/17 Chaos Eternal <chaose...@shlug.org>:

> scheme界有个神一样的存在，chez scheme, 号称跟C跑的一样快，但是没有source, 卖的还停贵的，显然有人买帳嘛。
> chez多快不知道， chez有个免费的解释执行版本，据说跑得已经比guile快很多了，然后chez作者的学生写了个ikarus,
> 经我实测确实很快（算fib比C慢30%,
> 而其他的scheme比C慢一个数量级），然后ikarus那哥们不做了，有人fork了个vicare出来，也挺快的。
> 话说，如果scheme能跟C做到类似的速度，谁还要用C++?!

Chez已经从王垠那里听说了。不过，我觉得算Fib不能说明问题。关键是复杂的数据结构能优化得多好。C靠程序员手砌高效的数据结构，C++提供了一大堆现成同时又性能不错的砖头。如果Scheme能直接根据高层的数据结构生成高效的底层实现，那就真该好好学习了。

--
Wu Yongwei
URL: http://wyw.dcweb.cn/

[Chaos Eternal]

不知道你说的数据结构是指树、栈、堆这种呢，还是指struct 。
如果是前者，scheme显然不会弱。
如果是后者，这就不好说了，具体一点？

2013/9/20 Yongwei Wu <wuyo...@gmail.com>:

[Yongwei Wu]

自定义数据结构，可以是结构，也可以是表（如果能够达到相似性能的话）。现实世界的数据结构。

我觉得要做试验的话，可能快速排序也比Fib要好。最经典而又简洁的函数式解法应该不会性能很好吧？

2013/9/22 Chaos Eternal <chaose...@shlug.org>:

[Chaos Eternal]

qsort.scm我有，谁来个C版的？

2013/9/22 Yongwei Wu <wuyo...@gmail.com>:

[Xidorn Quan]

写得丑莫见怪

void myqsort(int *arr, ptrdiff_t len)
{
ptrdiff_t i = 0, j = len - 1;
int m = arr[len / 2];

do {
while (arr[i] < m) i++;
while (arr[j] > m) j--;
if (i <= j) {
int tmp = arr[i];
arr[i] = arr[j];
arr[j] = tmp;
i++; j--;
}
} while (i <= j);

if (j >= 0) myqsort(arr, j + 1);
if (i < len) myqsort(arr + i, len - i);
}

2013/9/22 Chaos Eternal <chaose...@shlug.org>:

[Zhao Yibin]

c的stdlib里有qsort

[Xidorn Quan]

因为 C 能做的编译优化很有限，所以手写的特化版本一般会比 stdlib 里面的快一些。

我刚刚测了一下，在我这里，单考虑快排消耗的时间，我那个的速度比 stdlib 里的快了接近70%。
不过70%说实话我觉得已经挺好的了，我印象中以前好像是可以快几倍的，大概是编译器和库都有改进吧。

2013/9/23 Zhao Yibin <ybzha...@gmail.com>:

[Yongwei Wu]

我觉得很大一部分原因是使用qsort的话比较操作是一个函数调用吧。这个在C里很难被inline。这也是为什么C++里的sort算法比qsort通常更快的原因——模板可以把比较操作inline掉。

2013/9/23 Xidorn Quan <quanx...@gmail.com>:

[Xidorn Quan]

我同意。

不过其实拿出手写 qsort 更重要的一点是既然是比较代码性能，当然是要看得到明确的实现的。
无论是 C 的 qsort 还是 C++ 的 sort，它们的实现是什么样谁也不知道，一些细节方面不同的实现也存在差异。
比如说我印象中有些 C 的 qsort 并不是像我的程序中那样直接取中间值，而是取头、尾、中间三个值中的中间值。
C++ 的 sort 在一些实现上，除了 qsort 以外，还有结合归并排序以确保 nlgn 的运行时间。
如果变成这样的话，这就成了库的比较而不是代码性能的比较。

2013/9/23 Yongwei Wu <wuyo...@gmail.com>:

[yi lu]

听了各位大大的谈话，表示受益匪浅。
虽然不知道什么是形式逻辑（求指导），但是觉得作为一个数学专业渣渣，还是对Haskell很感兴趣的。

2013/9/23 Xidorn Quan <quanx...@gmail.com>

[Zhang Cheng]

2013/9/23 Xidorn Quan <quanx...@gmail.com>

不过其实拿出手写 qsort 更重要的一点是既然是比较代码性能，当然是要看得到明确的实现的。
无论是 C 的 qsort 还是 C++ 的 sort，它们的实现是什么样谁也不知道，一些细节方面不同的实现也存在差异。
比如说我印象中有些 C 的 qsort 并不是像我的程序中那样直接取中间值，而是取头、尾、中间三个值中的中间值。
C++ 的 sort 在一些实现上，除了 qsort 以外，还有结合归并排序以确保 nlgn 的运行时间。
如果变成这样的话，这就成了库的比较而不是代码性能的比较。

本科的时候，我做算法实验，读了好多版本的qsort，包括MSVC库、uclibc、glibc、stl等各种实现，分别都有一些不同，你感兴趣的话也都可以都去看一下。

所有这些qsort/sort在算法上区别不大，性能上，除了c++版本的以外，其他的都差不了多少，算法的区别不会是导致性能问题的关键，否则大家为啥不用同样的算法？

c比c++慢的根本原因是比较函数的调用，在c里面，比较函数是通过指针访问的，没办法inline，而C++用template，比较函数可以直接inline进去。

排序算法的基本操作就两个比较和移动​，移动这一块，只要数据结构相同（比如不要拿C的数组和C++的vector比较），那么移动的效率基本相同（都是用memmove来实现）。

比较这一块，指针跳转和直接inline相差就很大了，指针跳转对流水线、cpu缓存都有非常大的影响。

--

Cheng,

Best Regards

[David Pu]

比较操作不是个回调函数的话这个库函数就没什么用了，只能排序built-in的数据类型……

Xidorn Quan <quanx...@gmail.com>编写：

>我同意。

>
>不过其实拿出手写 qsort 更重要的一点是既然是比较代码性能，当然是要看得到明确的实现的。
>无论是 C 的 qsort 还是 C++ 的 sort，它们的实现是什么样谁也不知道，一些细节方面不同的实现也存在差异。
>比如说我印象中有些 C 的 qsort 并不是像我的程序中那样直接取中间值，而是取头、尾、中间三个值中的中间值。
>C++ 的 sort 在一些实现上，除了 qsort 以外，还有结合归并排序以确保 nlgn 的运行时间。
>如果变成这样的话，这就成了库的比较而不是代码性能的比较。
>

[none_nobody]

形式逻辑就是断言什么的，概念，概念的外延，推断，以及实现这些推断的方法，同一，确定，不矛盾等等。

比如 这样的概念及外延说话其中包含的逻辑 ：“所有金属都是导电的，镁是金属，所以镁是导电的”

“镁是活泼金属，活泼金属容易形成氧化层，氧化层是不良导体，所以对镁条的电阻测试过程中出现了奇怪现象。”

而我以为，prolog 或者 函数式编程在这个方向上介入过深 ，因为形式逻辑这事是关于思维的思维，二次元的思维，
不容易搞清楚，至少我以为目前人类对如何思维还不全面，更何况机器上的实现。

回到发贴处，是否可以通过最简短逻辑的堆叠，以及由外部导入的数据将简短逻辑的堆叠结果程式化，形成思维；

前面还发一个算24点的程序，程序运算的逻辑（人工编写的）就是将全部的输入数字和备选计算符号的排列，扫描符合的组合。这是一种固定输入（人工输入给定程序逻辑）；

如果写另一个程序，大量输入数据，随机选运算符号，计算结果对的情况下，将计算过程存储；
再有输入的时候，从已有的存储的计算过程中寻找可能的计算规律，输出的结果。这样就不走形式逻辑深挖的道路了。

就这样，不在形式逻辑上深入发展下去，而从输入的数据和基本的逻辑入手，让自然解决这个问题。

[Chaos Eternal]

2013/9/24 none_nobody <lyx...@gmail.com>:

> 形式逻辑就是断言什么的，概念，概念的外延，推断，以及实现这些推断的方法，同一，确定，不矛盾等等。
>
> 比如 这样的概念及外延说话其中包含的逻辑 ：“所有金属都是导电的，镁是金属，所以镁是导电的”
>
> “镁是活泼金属，活泼金属容易形成氧化层，氧化层是不良导体，所以对镁条的电阻测试过程中出现了奇怪现象。”
>
> 而我以为，prolog 或者 函数式编程在这个方向上介入过深 ，因为形式逻辑这事是关于思维的思维，二次元的思维，
> 不容易搞清楚，至少我以为目前人类对如何思维还不全面，更何况机器上的实现。
>

这个问题其实是哲学上的 逻辑推导到底是不是第一性的，还是后天习得的 。没法多作评论。

> 回到发贴处，是否可以通过最简短逻辑的堆叠，以及由外部导入的数据将简短逻辑的堆叠结果程式化，形成思维；
>
> 前面还发一个算24点的程序，程序运算的逻辑（人工编写的）就是将全部的输入数字和备选计算符号的排列，扫描符合的组合。这是一种固定输入（人工输入给定程序逻辑）；
>

就算24点来说，本人愚笨，只会穷举，不过练习多了呢，就习得一些特定的模式，然后一些问题就可以迅速套用模式得到答案。

> 如果写另一个程序，大量输入数据，随机选运算符号，计算结果对的情况下，将计算过程存储；
> 再有输入的时候，从已有的存储的计算过程中寻找可能的计算规律，输出的结果。这样就不走形式逻辑深挖的道路了。
>
> 就这样，不在形式逻辑上深入发展下去，而从输入的数据和基本的逻辑入手，让自然解决这个问题。

这个，我始终认为（12年前就跟你讲过），应该用马尔可夫模型，最好是可变长度的马尔可夫(vom)

>
>
>
> On Monday, September 23, 2013 2:33:52 PM UTC+8, timekeeper wrote:
>>
>> 听了各位大大的谈话，表示受益匪浅。
>> 虽然不知道什么是形式逻辑（求指导），但是觉得作为一个数学专业渣渣，还是对Haskell很感兴趣的。
>>
>>

[none_nobody]

关于二次元，这个词好，经常用。

弄Hadoop 的都知道 Meta-Data 吧， 就是关于数据的数据。写c++的 都会写 Template 吧，就是代码的代码。

还有思维的思维，程序逻辑的逻辑。而程序逻辑的逻辑，现在看到的还太少，Nero-Network 勉强算是一种，但这货过于纠缠在输入输出的数字上了。

[Xidorn Quan]

那个啥，qsort 不对比测试一下吗？

2013/9/24 Chaos Eternal <chaose...@shlug.org>:

[Chaos Eternal]

2013/9/24 Xidorn Quan <quanx...@gmail.com>:
> 那个啥，qsort 不对比测试一下吗？
>

没优化好呢。

qsort.scm:
(define (q-sort l)
(cond
[(null? l) '()]
[(null? (cdr l)) (list (car l))]
[else
(let ((small-part
(filter (lambda (x) (<= x (car l))) (cdr l)))
(big-part
(filter (lambda (x) (> x (car l))) (cdr l))))
(append
(q-sort small-part)
(list (car l))
(q-sort big-part)))]
)
)

但是这个版本问题有几个：
1. filter的实现问题
2. append的实现问题

因为对list的append是个O(m+n)的操作，不划算，我想写个用queue替换list的版本， 把append等操作的复杂度降下来，否则没有可比性。

queue是这样一个数据结构

((element1 . (element2 ... (elementN . ()))) . (elementN . ()))
; 也就是有一个指向尾巴的指针。

所以append就可以写成
(define (q-append! a b)
(begin
(set-cdr! (cdr a) (car b))
(set-cdr! a (cdr b))
a)
)

这就O(0)啦。

然后类似的写一个q-filter!
最后改写那个q-sort

然后么， scheme里面的List相当于C里面的链表，因此以上代码可以很容易写出C的对应版
最后才能做比较。



然后就是写个C语言的对应版。

[none_nobody]

论编程语言的算法效率，有专业的网站：

benchmarksgame.alioth.debian.org

上面可以任选常用算法的比较，大家就加血一次，以后不要再比拼qsort了，这种 Nlog2N的算法有什么好比拼的


On Monday, September 23, 2013 2:24:35 PM UTC+8, Xidorn Quan wrote:

我同意。

[Ray]

On 2013-09-23, none_nobody wrote:
>论编程语言的算法效率，有专业的网站：
>
>benchmarksgame.alioth.debian.org
>
>上面可以任选常用算法的比较，大家就加血一次，以后不要再比拼qsort了，这种 Nlog2N的算法有什么好比拼的
>

比較挺好的，其中有很多趣味性

比如常見的 SGI STL，sort 實現是 introsort，區間用兩個
RandomAccessIterator，但儘管如此，代碼中對 RandomAccessIterator \
ForwardIterator 特性的使用非常謹慎，不會出現像 `len - 1` 這樣的寫法

> ptrdiff_t i = 0, j = len - 1;

也會避免 `i <= j`，因爲想儘可能用 BidirectionalIterator 等高層 trait
就支持的東西

而且區間會儘量用左閉右開區間，我能想到的好處：

- hi - lo == size
- 區間合併自然

很多實現會儘量減少特殊情況的判斷，同時兼容區間爲空等例外情形，寫出這樣的程序是門藝術。

再如 Haskell、Erlang 等的 one-line(或兩行等等，總之爲了突出簡潔性)
sort，會創建很多中間列表，而非原地進行的，導致時間空間效率的降低

benchmarksgame 上的程序，很多都放棄了語言自身的特點，以
C/彙編 風格寫程序(比如 Haskell 的程序會用很多 Foreign.{Ptr,Storable,Marshal.Alloc}
和大量 unsafe 的東西)。rosettacode
看上去更友好一些，不過它沒有benchmark.......

[Yu Changyuan]

2013/9/24 none_nobody <lyx...@gmail.com>

形式逻辑就是断言什么的，概念，概念的外延，推断，以及实现这些推断的方法，同一，确定，不矛盾等等。

比如 这样的概念及外延说话其中包含的逻辑 ：“所有金属都是导电的，镁是金属，所以镁是导电的”

“镁是活泼金属，活泼金属容易形成氧化层，氧化层是不良导体，所以对镁条的电阻测试过程中出现了奇怪现象。”

而我以为，prolog 或者 函数式编程在这个方向上介入过深 ，因为形式逻辑这事是关于思维的思维，二次元的思维，
不容易搞清楚，至少我以为目前人类对如何思维还不全面，更何况机器上的实现。

 

我觉得， 对于程序设计来说，人类如何思维只是一方面。只有表达能力够强， 能够对目标问题方便快捷的建模，然后性能够高，就OK了（毕竟程序是用来解决问题的）。如果程序语言的设计还符合人类的思维方式（应该算认知心理学的范畴吧），那么编程的效率会提高、出错率则会降低。理想的程序设计语言应该是既和目标问题匹配，又符合思维，那么使用起来就会非常简单。

FP（lisp）和prolog早期都是搞AI的，我觉得出现这种情况应该是为了match目标问题的domain。

回到发贴处，是否可以通过最简短逻辑的堆叠，以及由外部导入的数据将简短逻辑的堆叠结果程式化，形成思维；

前面还发一个算24点的程序，程序运算的逻辑（人工编写的）就是将全部的输入数字和备选计算符号的排列，扫描符合的组合。这是一种固定输入（人工输入给定程序逻辑）；

如果写另一个程序，大量输入数据，随机选运算符号，计算结果对的情况下，将计算过程存储；
再有输入的时候，从已有的存储的计算过程中寻找可能的计算规律，输出的结果。这样就不走形式逻辑深挖的道路了。

就这样，不在形式逻辑上深入发展下去，而从输入的数据和基本的逻辑入手，让自然解决这个问题。

这个感觉像是神经网络，人脑的工作方式应该也是类似的吧。

下面是我的亲身经历：

没学编程前，觉得循环很抽象，后来学了C后，思维方式向循环靠拢了，很多问题自发的就按循环的逻辑来分解了（初值、下一状态、如何结束）。再后来，用了haskell，然后看问题的思路有变成递归了，甚至写C程序也会不小心写成递归风格。

也就是说，通过一段时间的训练，人的思维会对某种模式比较敏感（我的例子里面是循环或递归），并且会下意识的（自动的、不太费神的）对目标问题，分解成不同的要素，针对该模式进行匹配（感觉像是做大规模的并行搜索的样子）。

总的来说，这个应该是人脑的思路;从这种意义讲，形式逻辑什么的是”反人类“的。

On Monday, September 23, 2013 2:33:52 PM UTC+8, timekeeper wrote:

听了各位大大的谈话，表示受益匪浅。
虽然不知道什么是形式逻辑（求指导），但是觉得作为一个数学专业渣渣，还是对Haskell很感兴趣的。

--
-- You received this message because you are subscribed to the Google Groups Shanghai Linux User Group group. To post to this group, send email to sh...@googlegroups.com. To unsubscribe from this group, send email to shlug+un...@googlegroups.com. For more options, visit this group at https://groups.google.com/d/forum/shlug?hl=zh-CN
---
您收到此邮件是因为您订阅了 Google 网上论坛的“Shanghai Linux User Group”论坛。
要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 shlug+un...@googlegroups.com。
要查看更多选项，请访问 https://groups.google.com/groups/opt_out。

--
Best regards,
Changyuan

[Xidorn Quan]

为什么要按照 scheme 的思维方式写 C 的对应版？
之前说的不就是，既然很多人说 scheme 也可以被编译器优化的很快，那就看对于 qsort 这种算法，函数式能不能用更优雅的表达达到 C 做同样事情的效率。

[Xidorn Quan]

你搞错了，这里的 i 和 j 并不是组成一个区间用的，而是两个独立的指针下标：i 指针从头遍历，j 指针从尾遍历。所以 j 一开始就赋了 len - 1。
实际上我最早默 qsort 的时候，用的是闭区间 [l, r] 来表示排序范围，这样对于这个版本的算法来说，反而是写起来最方便的。

2013/9/24 Ray <i...@maskray.me>:

[none_nobody]

还真有非民科形制的名校课程，第20， Gentzen‘s Proof System.

http://www.cs.wm.edu/~idillig/cs780-02/

这个，我始终认为（12年前就跟你讲过），应该用马尔可夫模型，最好是可变长度的马尔可夫(vom)

真有 某人的 论文就是这么写的额：

http://homes.cs.washington.edu/~pedrod/papers/tlct.pdf

[Chaos Eternal]

2013/9/24 Xidorn Quan <quanx...@gmail.com>:

> 为什么要按照 scheme 的思维方式写 C 的对应版？
> 之前说的不就是，既然很多人说 scheme 也可以被编译器优化的很快，那就看对于 qsort 这种算法，函数式能不能用更优雅的表达达到 C 做同样事情的效率。

我不知道你的point在哪里，有写的很快的C，也有写的很慢的C，难道你认为只有C才允许在写的时候优化，而别的语言不准？
我写的第一版fib-c比比scheme跑的还慢，因为我不是个好码农，不知道这么说你满意了没有。。。

我之所以要说优化的事，是因为两个程序只有在算法上大致相当，才能比较，否则比什么呢？
说的更具体点，比如给你两个单向链表，只知道head的时候，你能在O(1)内把他们连起来么？但是如果同时给你这两个链表的tail,
问题就不一样了嘛。但是你会在所有的场合都要求有单链表的tail么？我看也不见得，特别是维护tail的时候带来的额外的复杂性，我看到了，你看到没有？

靠C/C++吃饭无可厚非，但是如果眼里只有C/C++，那估计也挺可悲的。

[Chaos Eternal]

>>
>
> 这个感觉像是神经网络，人脑的工作方式应该也是类似的吧。

神经网络如果经典的三层前馈结构的，那很容易训练，也很简单，但是能做的事情不多，至少不是图灵完全的；
如果是带回环的，那确实强大多了，而且图灵完全，但是很难训练；
其中研究的比较多了是long-short-term memory类的ANN，应用也有不少，不过我觉得这不就是一个有限深度的马尔可夫么。。

[Chaos Eternal]

2013/9/24 none_nobody <lyx...@gmail.com>:

二阶的不好玩，要http://en.wikipedia.org/wiki/Variable-order_Markov_model才好玩。
这个话题有一些变种，比如我前面说的long-short-term memory, 还有probabilistic-suffix-tree,
或者context-tree,
训练方法有winnow等算法。

[none_nobody]

二阶的不好玩，要http://en.wikipedia.org/wiki/Variable-order_Markov_model才好玩。
这个话题有一些变种，比如我前面说的long-short-term memory, 还有probabilistic-suffix-tree,
或者context-tree,
训练方法有winnow等算法。

这就俗了闹，做山贼也要有追求。

[none_nobody]

这里是刚挖掘来的开源项目

1.http://opencog.org
2 http://vicariousinc.com
3 https://github.com/tpsjr7/destin_ted_temp

[none_nobody]

居然链到 @周昌乐， 原来一直以为他的项目和类似就是大民科，其实人家道行还是有的。

On Tuesday, September 24, 2013 9:53:59 PM UTC+8, none_nobody wrote:

这里是刚挖掘来的开源项目

[Xidorn Quan]

2013/9/24 Chaos Eternal <chaose...@shlug.org>:
> 2013/9/24 Xidorn Quan <quanx...@gmail.com>:

>> 为什么要按照 scheme 的思维方式写 C 的对应版？
>> 之前说的不就是，既然很多人说 scheme 也可以被编译器优化的很快，那就看对于 qsort 这种算法，函数式能不能用更优雅的表达达到 C 做同样事情的效率。
>
> 我不知道你的point在哪里，有写的很快的C，也有写的很慢的C，难道你认为只有C才允许在写的时候优化，而别的语言不准？
> 我写的第一版fib-c比比scheme跑的还慢，因为我不是个好码农，不知道这么说你满意了没有。。。
>
> 我之所以要说优化的事，是因为两个程序只有在算法上大致相当，才能比较，否则比什么呢？
> 说的更具体点，比如给你两个单向链表，只知道head的时候，你能在O(1)内把他们连起来么？但是如果同时给你这两个链表的tail,
> 问题就不一样了嘛。但是你会在所有的场合都要求有单链表的tail么？我看也不见得，特别是维护tail的时候带来的额外的复杂性，我看到了，你看到没有？

没有不允许你写的时候优化，我也希望你能写出一个最优化的 scheme 版本来做比较。
我想说的是，本身使用每个语言的思路就是不一样的，如果要比做一件事情的效率，当然是拿出两个语言最优化的方案来比，而不是为了比较，而要求另一方有意改用一个次优化的实现方式。

> 靠C/C++吃饭无可厚非，但是如果眼里只有C/C++，那估计也挺可悲的。

不好意思，我不靠 C/C++ 吃饭。

[Chaos Eternal]

2013/9/24 Xidorn Quan <quanx...@gmail.com>:

完全没有说用C的次优化来比的意思。只是希望尽量有可比性。

>
>> 靠C/C++吃饭无可厚非，但是如果眼里只有C/C++，那估计也挺可悲的。
>
> 不好意思，我不靠 C/C++ 吃饭。

当我没说。

[liyaoshi]

在 2013年9月25日上午8:34，Chaos Eternal <chaose...@shlug.org>写道：

2013/9/24 Xidorn Quan <quanx...@gmail.com>:

> 2013/9/24 Chaos Eternal <chaose...@shlug.org>:
>> 2013/9/24 Xidorn Quan <quanx...@gmail.com>:
>>> 为什么要按照 scheme 的思维方式写 C 的对应版？
>>> 之前说的不就是，既然很多人说 scheme 也可以被编译器优化的很快，那就看对于 qsort 这种算法，函数式能不能用更优雅的表达达到 C 做同样事情的效率。
>>
>> 我不知道你的point在哪里，有写的很快的C，也有写的很慢的C，难道你认为只有C才允许在写的时候优化，而别的语言不准？
>> 我写的第一版fib-c比比scheme跑的还慢，因为我不是个好码农，不知道这么说你满意了没有。。。
>>
>> 我之所以要说优化的事，是因为两个程序只有在算法上大致相当，才能比较，否则比什么呢？
>> 说的更具体点，比如给你两个单向链表，只知道head的时候，你能在O(1)内把他们连起来么？但是如果同时给你这两个链表的tail,
>> 问题就不一样了嘛。但是你会在所有的场合都要求有单链表的tail么？我看也不见得，特别是维护tail的时候带来的额外的复杂性，我看到了，你看到没有？
>
> 没有不允许你写的时候优化，我也希望你能写出一个最优化的 scheme 版本来做比较。
> 我想说的是，本身使用每个语言的思路就是不一样的，如果要比做一件事情的效率，当然是拿出两个语言最优化的方案来比，而不是为了比较，而要求另一方有意改用一个次优化的实现方式。

完全没有说用C的次优化来比的意思。只是希望尽量有可比性。

>
>> 靠C/C++吃饭无可厚非，但是如果眼里只有C/C++，那估计也挺可悲的。
>
> 不好意思，我不靠 C/C++ 吃饭。

当我没说。

你伤害了我，却一笑而过

[Chaos Eternal]

>
> 你伤害了我，却一笑而过
>

我错了

[none_nobody]

如果将 linux kernel 函数生成一大的graph. 函数名当成节点，调用关系当做成边。这样在这个图里搜索是不是能提示点什么。

之所以这么想，觉得这事是应该有人已经这么做过了，想看一下结果。知道的出来所所。

On Wednesday, September 25, 2013 8:53:22 AM UTC+8, Soahc Lanrete wrote:

>
> 你伤害了我，却一笑而过
>

我错了

[none_nobody]

大家感受一下。

http://www.cs.umd.edu/hcil/millionvis/Treemap_Visualization_of_the_Linux_Kernel_2_5_33.html

[none_nobody]

果真就是这个了。

http://gource.googlecode.com/svn/trunk/gource-linux.jpg

[none_nobody]

不仅静态有，动态的也有。

http://people.redhat.com/srostedt/kernelshark/HTML/

On Thursday, September 26, 2013 11:15:23 AM UTC+8, none_nobody wrote:

果真就是这个了。

[david pu]

kernelshark只是个debug工具，ftrace的GUI front end, ftrace可以tracekenrel 的 function/event或function graph. 其实就是利用gcc的-finstrument-functions选项做的。自己也在自己的bootloader里搞过同样的东西并用dot画成图，即使是这个只有1个task加中断的流程，画出来的图也十分凌乱。。

--
-- You received this message because you are subscribed to the Google Groups Shanghai Linux User Group group. To post to this group, send email to sh...@googlegroups.com. To unsubscribe from this group, send email to shlug+un...@googlegroups.com. For more options, visit this group at https://groups.google.com/d/forum/shlug?hl=zh-CN
---
您收到此邮件是因为您订阅了 Google 网上论坛的“Shanghai Linux User Group”论坛。
要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 shlug+un...@googlegroups.com。
要查看更多选项，请访问 https://groups.google.com/groups/opt_out。

--
 ()   ASCII Ribbon Campaign
 /\   Keep it simple!

[none_nobody]

那个啥，说到快排，CPU cache 还是影响很大的。如果 100k 以下的items , 基本上还是会受CPU Cache 影响。效率比直接使用指针地址会提高150-200 倍。如果超过 200k items , 多线程快排会开始好起来。

如果直接引用随机分配的地址，会慢的要命。

数据是比如，这样的形式。

struct list {

 struct list *prev, *next;

 void *value;

}

如果用 cmp 函数是
int compare(const void *arg1, const void *arg2)
{
     return (  *(int *)(arg1)  >  *(int *)(arg2) );
}

On Tuesday, September 24, 2013 1:15:41 PM UTC+8, Xidorn Quan wrote:

那个啥，qsort 不对比测试一下吗？

[liyaoshi]

100K？ 

zlib 有个arm neon 的优化测试结果

同频A8居然比A9快

惊讶吧

cortexA8 cacheline 是64bit的

cortexA9  cacheline 是32bit的

坑爹么？

[liyaoshi]

更正一下 是byte不是bit

[none_nobody]

就是 list 中 十万个项了。A8 A9 快多少，不过一个用CPU Cache ，一个不用，差上百倍还是惊到我了。

要是差百分之几十页也就算数了。

继续歪楼，水果公司才上A7-64 ，这个水果的 A7 是啥么稿？ arm 里算几？



On Wednesday, October 9, 2013 1:05:14 PM UTC+8, liyaoshi wrote:

100K？ 

[Grissiom]

2013/10/9 none_nobody <lyx...@gmail.com>

就是 list 中 十万个项了。A8 A9 快多少，不过一个用CPU Cache ，一个不用，差上百倍还是惊到我了。

用 cache 不用 cache 差百倍应该也在预料之内，因为内存的访问要比 cache 的访问慢几个数量级吧……

 

要是差百分之几十页也就算数了。

继续歪楼，水果公司才上A7-64 ，这个水果的 A7 是啥么稿？ arm 里算几？

算 ARMv8 吧……

 

On Wednesday, October 9, 2013 1:05:14 PM UTC+8, liyaoshi wrote:

100K？ 

--
-- You received this message because you are subscribed to the Google Groups Shanghai Linux User Group group. To post to this group, send email to sh...@googlegroups.com. To unsubscribe from this group, send email to shlug+un...@googlegroups.com. For more options, visit this group at https://groups.google.com/d/forum/shlug?hl=zh-CN
---
您收到此邮件是因为您订阅了 Google 网上论坛的“Shanghai Linux User Group”论坛。
要退订此论坛并停止接收此论坛的电子邮件，请发送电子邮件到 shlug+un...@googlegroups.com。
要查看更多选项，请访问 https://groups.google.com/groups/opt_out。

--
Cheers,
Grissiom

[Grissiom]

2013/10/9 none_nobody <lyx...@gmail.com>

就是 list 中 十万个项了。A8 A9 快多少，不过一个用CPU Cache ，一个不用，差上百倍还是惊到我了。

要是差百分之几十页也就算数了。

继续歪楼，水果公司才上A7-64 ，这个水果的 A7 是啥么稿？ arm 里算几？

全志还有 A20 呢…… http://www.allwinnertech.com/product/A20.html

--
Cheers,
Grissiom

[liyaoshi]

WO KAO

全志那是为了淘宝上面的卖家做图片的时候号码显得大 ，好卖吧

armV8 应该是从corexA57开始

--

[liyaoshi]

说到全至，A20那么火的玩意，后面就熄火了

话说，ARM这块，现在除了高通，三星，苹果，有卖芯片挣钱的么？

[Grissiom]

2013/10/9 liyaoshi <liya...@gmail.com>

WO KAO

全志那是为了淘宝上面的卖家做图片的时候号码显得大 ，好卖吧

armV8 应该是从corexA57开始

如果是 64 位的，那么肯定是 ARMv8。Cortex-A57 只是 ARM 出的。

哦，这里 ARMv8 是指令集，而不是架构。那个 A7 的架构是它自己的？这个就不清楚了……

--
Cheers,
Grissiom

[Grissiom]

2013/10/9 liyaoshi <liya...@gmail.com>

说到全至，A20那么火的玩意，后面就熄火了

话说，ARM这块，现在除了高通，三星，苹果，有卖芯片挣钱的么？

除了 AP，还有 MPU，Cotex-M0/M3/M4，厂商有 TI/ST/freescale/…… 还有各种其他芯片内嵌 ARM 核的…… 之前不是有人破解硬盘控制器，发现里面是个双核的 ARM9 么……

--
Cheers,
Grissiom

[liyaoshi]

三星的 硬盘很多是arm7的,

cortex A9 太贵了吧， 或者你说的是ssd ？

话说卖A8 A9的，出个200w片，大家多觉得很牛逼的量了，买个m0 ,200w片，根本赚不到啥钱啊 0.34美元一个stm32 F0 ，卖个200万片，还不够上海中环一套房子值钱

[Grissiom]

2013/10/9 liyaoshi <liya...@gmail.com>

三星的 硬盘很多是arm7的,

cortex A9 太贵了吧， 或者你说的是ssd ？

ARM9 不是 A9 啊……

话说卖A8 A9的，出个200w片，大家多觉得很牛逼的量了，买个m0 ,200w片，根本赚不到啥钱啊 0.34美元一个stm32 F0 ，卖个200万片，还不够上海中环一套房子值钱

ST 的 MCU 是亏钱的…… 不过还有其他的厂商在做，其他的就不清楚了……

--
Cheers,
Grissiom

[liyaoshi]

如果ST多亏钱，其他谁能赚钱？感觉就ARM自己赚钱了

是ST 里面人工钱太高了？

MCU这一块，有挣钱的人家么？瑞萨多不挣钱

[Xuangui Huang]

Another interesting book....
" Software Foundations"

2013/9/17 Chaos Eternal <chaose...@shlug.org>

我倒是有本书，叫 《程序设计语言的形式语义》， 不过还没啃完。

http://www.amazon.cn/%E7%A8%8B%E5%BA%8F%E8%AE%BE%E8%AE%A1%E8%AF%AD%E8%A8%80%E7%9A%84%E5%BD%A2%E5%BC%8F%E8%AF%AD%E4%B9%89-Glynn-Winskel/dp/B0011AN65Y/ref=sr_1_1?ie=UTF8&qid=1379397127&sr=8-1&keywords=%E7%A8%8B%E5%BA%8F%E8%AE%BE%E8%AE%A1%E8%AF%AD%E8%A8%80%E7%9A%84%E5%BD%A2%E5%BC%8F%E8%AF%AD%E4%B9%89

将这个问题讲的比较深入。你要来拿。

然后关于谓词逻辑的语言，真心推荐prolog, 当然根据前文，用scheme也能实现prolog能实现的。
还有ACL2 (A Computational Logic for Applicative Common Lisp) is a
software system consisting of a programming language, an extensible
theory in a first-order logic, and a mechanicaltheorem prover.

我最近到确实在考虑对写的代码做形式证明的事情：
比如对于函数 f :N -> N （考虑到大部分的程序其实都是做这事的，我就简化一下）
用归纳法， 先证明f(1) 成立，然后证明若 f(k)成立则f(k+1)也成立，
后面这个就需要对f(k+1)进行形式转换，然后演绎证明了。
当然这涉及到高阶函数啊，alpha,beta, gamma变换啊等等，所以只是个想法，哈哈。
还是那句话，一起玩啊




2013/9/17 none_nobody <lyx...@gmail.com>:

> 先说，形式逻辑，基本语意定义上有概念、定义、判读、推论、演绎，推理（走的太远了）
>
> 自我构建是说，在给定（限定范畴）概念、定义、判断、推论的前提下，运行中形成模式化演绎或则归纳的结构，而无需人工编码。
>
> 如上述运行中形成.....人工编码不能实现。
>
> 则在函数式编程中，归纳和推理是如何做的，包括
> 基本逻辑 ： 同一、不矛盾、排中、充足理由。
>
> 举例：一种定义  Add ( +  int, int)  可以视为形式逻辑定义了一种概念  UserDefined_Oper (
> "oper_character" ,  ”type", "type" )， 同一概念是指：视 UserDefined_Oper 为 A ,  A->A,
> 这种  [ UserDefined_Oper ] 不可变，
>
> 粗略地说，是在 L2 上 UserDefined_Oper 去多态性。
>
> 在归纳演绎时，有如下过程 ： 概念（定义）得到  推论。
>
> 我的问题在指这里如何定义这个归纳演绎的这个过程，或者程序运行中自动能构成归纳（自构建）
> 相应的还有类比推理、假设推理等。
>
> 上述的在这里可以类比于图结构学习中，在运行中调整节点和边的联系，形成的形式归纳。
>
>
>
> On Tuesday, September 17, 2013 11:07:46 AM UTC+8, Soahc Lanrete wrote:
>>
>> 先题外话：窃以为haskell的函数式太纯粹了。
>>
>> 然后不太明白你说的自我构建是什么意思，如果你是说first-class-function，那是所有的函数式都有的，类似的还有 currying
>> 这些。
>> 然后函数就可以返回一个函数然后再返回一个函数去计算你要的东西，当然闭包特性在这里起了很大的作用。

[none_nobody]

Chipworks通过A7分析后得出，它是一款基于28nm工艺制程的双核处理器（ARM v8架构，主频为1.3GHz），内置的GPU为四核心（Power VR G6430），同时他们还发现了Secure Enclave（安全区域），而该区域就是苹果之前说的存储加密指纹数据的地方。

此外，A7中的安全区域中还拥有至少3MB的SRAM（静态随机存储器，不需要刷新电路就能保存存储数据），同时Chipworks还表示这款64位处理器的设计与A5、A6和A6X有相同的地方，如USB、LCD和相机接口。

  与此同时，Chipworks还猜测A7处理器CPU核心可能整合了256KB的L1高速缓存和1MB的L2高速缓存，而双核CPU和高速缓存占据了模具区域17%的面积，而四核GPU以及共用逻辑占据大约22%的面积。

  之前，Chipworks给出的结论还显示，A7是由三星代工制造的，而5S的拆解则显示，M7协处理器其实就是NXP LPC18A1。

L1 比我的PPC 7455 大。Level 1 Cache: 32 kB data, 32 kB instruction Level 2 Cache: 256 kB on-cpu。L1 超过推土机了。

[Grissiom]

2013/10/11 none_nobody <lyx...@gmail.com>

Chipworks通过A7分析后得出，它是一款基于28nm工艺制程的双核处理器（ARM v8架构，主频为1.3GHz），内置的GPU为四核心（Power VR G6430），同时他们还发现了Secure Enclave（安全区域），而该区域就是苹果之前说的存储加密指纹数据的地方。

此外，A7中的安全区域中还拥有至少3MB的SRAM（静态随机存储器，不需要刷新电路就能保存存储数据），同时Chipworks还表示这款64位处理器的设计与A5、A6和A6X有相同的地方，如USB、LCD和相机接口。

外设相同还是挺正常的，这样可以简化驱动的编写～不过这个 SRAM 可是够大的…… 

  与此同时，Chipworks还猜测A7处理器CPU核心可能整合了256KB的L1高速缓存和1MB的L2高速缓存，而双核CPU和高速缓存占据了模具区域17%的面积，而四核GPU以及共用逻辑占据大约22%的面积。

  之前，Chipworks给出的结论还显示，A7是由三星代工制造的，而5S的拆解则显示，M7协处理器其实就是NXP LPC18A1。

L1 比我的PPC 7455 大。Level 1 Cache: 32 kB data, 32 kB instruction Level 2 Cache: 256 kB on-cpu。L1 超过推土机了。

不过话说这个讨论“形式逻辑”的帖子被歪成芯片贴了呃……

--
Cheers,
Grissiom

[none_nobody]

这种叫激发人气，吸引相关人等自驱动推荐进入话题。话说，编程这事，考虑的是怎么 “进行” 计算。 所以真正的程序员都会对人为什么“会思考” 这事感兴趣。

在计算机程序实现过程中，通常就是用基本的逻辑把数据处理成对应的结果。比如计算24点，而在处理过程中，整个”处理的过程“被固化，而且默认是不可见的丢失。

如同思考“为什么会思考”的过程建立起来的形式逻辑系统，这个形式逻辑相当于编程时用的基本逻辑过程，而形式逻辑的深入探究过程，或忽略的用基本逻辑处理的数据的中间过程。

现在计算机的能力膨胀和并行化多主机技术的发展，已经可以让一些小型的题目的“处理过程”存储下来。说到底是我觉得对付“处理过程”是比较有意思的事。数据基本结构的链表图上的结构学习过程，有些代码可以写。

比如这样的，用数据建立起一个图，1M 个顶点，1G条边，然后将这个图的谱弄出来，写个代码来瞧瞧。

[none_nobody]

s/或忽略的用/或忽略了用/g

[liyaoshi]

我很好奇这个图，跟乌鸦在没有月亮的晚上飞，有啥两样？

--

[Chaos Eternal]

没有月亮还有星星啊，没有星星可以用雷达啊，总之只要那里"确实"有只乌鸦，总有办法看到的嘛。

2013/10/11 liyaoshi <liya...@gmail.com>:

[none_nobody]

其实就是乌鸦暗夜飞啊，一只乌鸦是看不出来什么道理的，要是上万只乌鸦一起飞，总有是飞回到该去的地方的吧。

众多的逻辑又或者是运算的关系，单个来看只是随机的猜。如果有一个叫损失函数的东西去判别哪些随机才的比较准的话，就可以建立起一个标准。要是很多很多个猜的过程汇集在一起的话，也许就能计算了吧。

要是点 Y   到   点  Y  的 概率，比点 Y 到点 D 的概率高一点点的话，或者就能表示整体中YY比YD 好那么一丁点丁点。



On Friday, October 11, 2013 12:37:29 PM UTC+8, liyaoshi wrote:

我很好奇这个图，跟乌鸦在没有月亮的晚上飞，有啥两样？

[none_nobody]

要是不信，你算个题目，从1到1000，用程序全扫不论用加减乘数，得数要算出1000来。

要是人算就很简单，（1+2-3）*4*5*6*7.... *999 + 1000 = 1000

呵呵，这样算么？

On Friday, October 11, 2013 1:12:01 PM UTC+8, none_nobody wrote:

其实就是乌鸦暗夜飞啊，一只乌鸦是看不出来什么道理的，要是上万只乌鸦一起飞，总有是飞回到该去的地方的吧。

[Chaos Eternal]

你的意思是，先找出1000, 然后在剩下的数里面凑个0出来，最后把所有余下的数跟这个0相乘再加上那个1000, 就完事了？

你想证明的是，用程序没法实现这个思维过程？

2013/10/11 none_nobody <lyx...@gmail.com>:

[none_nobody]

收起背包，就用 for 循环扫描数字和算符，应该是不行的吧。

[Chaos Eternal]

问题是，你不愿意做遍历的，计算机就愿意做？

2013/10/11 none_nobody <lyx...@gmail.com>:

[none_nobody]

要么怎么说是在写程序呢，需要程序员们想出一个好的数据结构，这还不算，还要想出好的节奏。

脑子应该不是这么做的，它是学出来的，来些数据，再来些指教，这样对那样错，对了有奖，错了打手心，给脸色，言语批评。好记下了，这中间有些什么规律可以找出来呢？ 这样、那样，哦突发奇想组合（随机挑选）一个，这样也是对的会有奖。

然后就会了。都不用被另外一个碳水化合物胶质体用压力、波、射线用1001规则化执行路线。

[none_nobody]

On Friday, October 11, 2013 1:55:07 PM UTC+8, Soahc Lanrete wrote:

你的意思是，【先找出1000, 然后在剩下的数里面凑个0出来，最后把所有余下的数跟这个0相乘再加上那个1000 】, 就完事了？

这个中括号【】之间 的过程，难道不能让程序运行的时候建立出来？二次编程，编一个 [ 建立 ] 这种思路的过程。

而不是把思路写死在代码里。

[Zang MingJie]

这题目动态规划不是秒解么？

[none_nobody]

有动态规划不能秒解的题目么？比如 ，这个图的物品的识别解释。



On Friday, October 11, 2013 2:33:47 PM UTC+8, Zang MingJie wrote:

这题目动态规划不是秒解么？

[Chaos Eternal]

任何一个用人侧脸过度训练的神经网络都可以找到那两个人脸。

任何一个用酒杯（痰盂）过度训练的神经网络也可以找到那个痰盂。

2013/10/11 none_nobody <lyx...@gmail.com>

[none_nobody]

请教有人做过Graph adjacency matrix，这种啥个情况，怎么解释怎么用啊？

给科普一下知识呗。