Confronting Two Trees

[alex.ch...@iohk.io]

Say I have two trees(a proposition tree starting with R and a proof tree starting with RP) like:

    R                                       RP
  /    \                                    /    \
L1   L2                                LP1 LP2

Where RP is a "proof" for R etc (node types could be different).

I want to confront the two trees as follows:

1. Check whether they have exactly the same shape
2. Check a node in some position in the proof tree corresponds to a node in the "proposition" tree

What is the most Kiama-idiomatic way to do that(I'm on Kiama 2.0.0)


sincerely, Alexander

[Meredith Gregory]

Dear Alex,

Independent of kiama, you probably want to calculate bisimulation, here.

R ≈ RP ⇔ ∀e. e( R, R' ) ∃e'. e'( RP, RP' ) with R' ≈ RP'

and vice versa.

There's a lot of information about efficient algorithms for bisimulation. Here's one reference. You might begin with Paige-Tarjan and then look at more modern techniques. Once you've selected the algorithm, rendering it in idiomatic kiama should be relatively straightforward.

Best wishes,

--greg

--
You received this message because you are subscribed to the Google Groups "kiama" group.
To unsubscribe from this group and stop receiving emails from it, send an email to kiama+unsubscribe@googlegroups.com.
To post to this group, send email to ki...@googlegroups.com.
Visit this group at https://groups.google.com/group/kiama.
For more options, visit https://groups.google.com/d/optout.

--

L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SW

Seattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com