Talk:Böhm tree

References

Can Barendregt's book from 1984 be cited as a good reference here? (I don't have a copy with me, but it's definitely worth checking) Hritcu (talk) 14:41, 18 January 2011 (UTC)[reply]

Here is another reference that might be relevant: Soren B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In Mathematical Foundations of Programming Semantics, volume 20 of Electronic Notes in Theoretical Computer Science, pages 346–374. Elsevier Science, April 1999 Hritcu (talk) 14:45, 18 January 2011 (UTC)[reply]

Rough ideas for making the article more accessible

Suggest something like,

Introduction

Value of a lambda term represented as a list where each element can be a list (a tree structure)
Sub lists that are the same are merged.
This is a DAG
Explain that we need to be able to access individual sub trees, even if the whole structure is not built.
Explain link between lists and lambda terms
Beta reduction applied to individual sub trees leads to what ...

Informal Definition

pretty much as is,

Example

Worked example

Thepigdog (talk) 23:37, 16 January 2014 (UTC)[reply]

The article definitely needs worked examples. I need to figure out a good way to draw diagrams! I'm less comfortable with the list idea though, because although the idea of a Bohm tree implies a way to "build" them, the "building" is actually a procedure for finding them; as mathematical objects they kind of "already exist" once they are defined. My feeling is that this distinction is important for infinite objects, because such objects can (and are) defined, but can't effectively be built. That's why I informally invoke the notion of the procedure "in the limit"; in fact it's mainly this that makes the definition informal. A formal definition requires either "jumping" directly to the object, or being precise about what the limit is. Haklo (talk) 23:54, 19 January 2014 (UTC)[reply]

I have trouble understanding a DAG, but I am quite comfortable with a tree structure in which part of the tree structure is repeated. A pointer to a repeated tree structure is easy to understand.

In detail you are describing a tree structure which is being evaluated. The order of evaluation must be breadth first in some way. Again that is sort of OK.

I dont understand in detail what a Bohm tree is. I have a general picture but the detail is not clear,

I suggest you don't mention infinity at all. Better to describe it in terms of lazy evaluation.

Diagrams

Diagrams are very useful but hard to do well. They are best used to give a general description.

The tools I have seen used are Dia and visio.

A picture may give an immediate insight. However I have not found a general visual language that is useful. The best diagrams appear to be the ones written on knapkins, after a few bottles of red wine.

Diagrams are then either too restricted or cluttered, or too adhoc. I wish I had better answers on this question.

A couple more points. The idea of the DAG already existing is Platonic. However I suggest you dont describe it in those terms. I see the recipe for creating the structure but I dont picture the infinite list as existing. Instead I picture the parts of the structure that are needed being constructed on demand as needed, as in lazy evaluation.

Thepigdog (talk) 12:07, 6 February 2014 (UTC)[reply]

I dont really have a clear picture of Bohm tree yet. Your example gives a list (of digits structure). But in general it is more tree like. Would another suitable example be something like Pascals triangle?

Maybe you could explain the Bohm tree to me here.

Some questions:

who would use a Bohm tree (is a mathematical construct only).
why is it needed?
why does it have to be a graph structure?
is it really a particular representation of a possibly infinite lambda expression?

Maybe by explaining it to me here you will work out how to make the article easy to understand.

A lambda expression that never terminates produces absolutely nothing if only a normal form is a value. This is clearly wrong.

Using the additive formula for pascals triangle. One lambda expression could give a list of lists representation of Pascals triangle. This could be represented as Bohm tree. Another lambda expression could be applied to the Bohm tree to retrieve a value. This might demonstrate the essential characteristics of a Bohm tree. A Bohm tree represents the communication between too systems. Pascals triangle could be encoded as a calculation with Church numerals and lists.

Regards Thepigdog (talk) 13:59, 10 February 2014 (UTC)[reply]