Proofs and computation with trees

栏目: IT技术 · 发布时间: 5年前

内容简介:In this post, I will make the analogy between trees and proofs and computation.Lately (after aA tree is a structure that represents hierarchical data. Here is one possible tree:

In this post, I will make the analogy between trees and proofs and computation.

Lately (after a long pause ), I started reading Logical Foundations again and started re-doing the exercises for the latest version (6.5). While doing the proofs this time, I kept thinking about tree traversals, so that inspired me to write this post.

Trees

A tree is a structure that represents hierarchical data. Here is one possible tree:

2
 / \
1   3

The meaning of the hierarchy, or the connection between the nodes, is defined by us. In the tree above, the meaning is “the left branch is less than the root, and the right branch is greater than the root”. The tree traversal operation can also be defined by us (such as print the current node, or execute it, etc).

Proof trees

Allowing us to define these meanings is what makes trees interesting. One application is the so-called proof trees , which allow us to validate logical arguments for mathematical proofs. Some examples that allow us to specify and traverse this type of tree are theorem provers such as Coq .

Proofs and computation with trees
Proof tree – Image courtesy of Logicmatters.net

Computation trees

Another application is the Computation tree , which allows us to mimic any computation. In this case, the traversal is the “execution” of the code. Some examples that allow us to specify and traverse this type of tree are Lisp-like programming languages, such as Racket .

Proofs and computation with trees
Lisp program – image courtesy of shrager.org

Proofs

In the Tactics chapter of Logical Foundations, there’s a section “Varying the Induction Hypothesis” that’s discussed. For example, if we want to prove Proofs and computation with trees , we introduce and and use induction on . But, the proof will be impossible because we cannot use the inductive hypothesis on the goal. So we “backtrack” (traverse up) in the tree of *all possible proofs* and take a different branch to attempt the proof. If we avoid introducing the variable , and use Proofs and computation with trees as the inductive hypothesis, we will be able to complete the proof.

Computation

Did the previous paragraph sound confusing? I will make the analogy with my favorite time killer game – Spider Solitaire .

Proofs and computation with trees

Observe how I start by moving the 4♠ from the 1st column to the 8th column. This move will reach the end of the tree without any substantial progress. But, when I undo the move (traverse up in the tree) and take a different direction by moving the 4♠ from the 2nd column to the 8th column, then things bloom and this branch of the tree is far more successful.

Conclusion

How does one find the most successful branches in advance? I think that comes with experience, but also luck, because sometimes you just don’t know what’s behind the cards unless you open them. This is why mathematical proofs, programming, and (some) games are not that easy of a challenge.

In any case, it was interesting to make this connection


以上就是本文的全部内容,希望对大家的学习有所帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

创业维艰

创业维艰

本·霍洛维茨 Ben Horowitz / 杨晓红、钟莉婷 / 中信出版社 / 2015-2 / 49

本·霍洛维茨,硅谷顶级投资人,与网景之父马克·安德森联手合作18年,有着丰富的创业和管理经验。2009年创立风险投资公司A16Z,被外媒誉为“硅谷最牛的50个天使投资人”之一,先后在初期投资了Facebook、Twitter、Groupon、Skype,是诸多硅谷新贵的创业导师。 在《创业维艰》中,本·霍洛维茨从自己的创业经历讲起,以自己在硅谷近20余年的创业、管理和投资经验,对创业公司(尤......一起来看看 《创业维艰》 这本书的介绍吧!

URL 编码/解码
URL 编码/解码

URL 编码/解码

XML 在线格式化
XML 在线格式化

在线 XML 格式化压缩工具

Markdown 在线编辑器
Markdown 在线编辑器

Markdown 在线编辑器