Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] The internal implementation of Isabelle (ML) t...

Email Gateway (Apr 02 2022 at 13:49):

From: Li Yongjian <lyj238@gmail.com>
Dear authors:
Here I want to ask questions on the internal implementation of Isabelle
(ML)
terms.

let t= a+b in
t*t;

(a+b)*(a+b)

the first term contains only one copy of (a+b), but the second term
contains two copies of (a+b).

In my understanding, the first term is stored as figure (a), the second
is stored as figure (b).

Is my understanding correct?

[image: image.png]

regards!
lyj
image.png

Email Gateway (Apr 02 2022 at 13:52):

From: Peter Lammich <lammich@in.tum.de>
Hi Li,

this depends on the internals of the underlying SML implementation.

PolyML will share some terms, but that's not guaranteed. From the view
of ML, this kind of sharing is not visible.
image.png

Email Gateway (Apr 02 2022 at 13:54):

From: Makarius <makarius@sketis.net>
This depends on many side-conditions, e.g. expanding the let via (simp add:
Let_def) will rather quickly cause duplications.

And on the contrary: a term with duplicate subterms can be stored in memory
without duplicates (the ML program will not see this).

Or maybe you just want to see the symbolic datatype of terms (or types)? You
can do it like this:

ML ‹
val t1 = @{term "let t= a+b in t*t"};
val t2 = @{term "(a+b)*(a+b)"};
›

See also the "implementation" manual, chapter 2.

Makarius

Last updated: Jul 15 2022 at 23:21 UTC