Subject: Fragments

Keywords: ::overview
          ::alpha
          ::normal

Title: Alpha normalized fragments

--------------------------------------------------

Abstract with respect to relative hyp order and variable names.
   
 Layers :
   - Hyps are grouped by binding layer.
    Consider a free variable in a hyp term
     that constitutes an edge in a graph from hyp-id to free var (which
     is itself a hyp-id of earlier hyp).
    these edges form a forest, group path maximum path length that of 
    paths starting at hyp.

 h1: T()
 h2: T(h1)
 h3: T()
 h4: T(h3,h2)

 Graph:  (2,1), (4,3), 4,2)
   - note that h4 has two paths [(4,3)] and [(4,2); (2,1)]

 L0 : h1,h3
 L1 : h2
 L2 : h4

 Within a layer order is arbitrary.

 Why : supposing that the layer structure is a searchable characteristic.
  the layers of any possible match must have some relation to the layer
  of the target fragment.
  
 Sort : 
  - currently does sort based on var name.
  - better to randomize within layers.
  ? Sort does produce predictable order, but can think of no value to that. 

 Hyp Order : some tactics do depend on order.
  ! As order is arbitrary not wrong to not permute, but then when using
    fragment must reorder instance sequent to match fragment
    This is not optimal.
  - minus_one : some tactics manipulate last hyp
  - MoveToConcl : if you permute hyps then MoveToConcl will make concl that is not
                  alpha equalent to non permuted sequent.
      * grind skips sort
      * hyps may still move due to layering.  

 Variable names are always regenereated base
  - binding
  - layer
  - original order?
    better would be :  
      * term size of type term
      * some term sig ordering.
⋅
--------------------------------------------------

Authors: NUPRL:t

⋅

Home