Subject: Fragments

Keywords: ::algorithm
          ::implementation

Title: Fragment equality and matching functions

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

Equality :
 dups, 

Match : 
 - match sequent to instantiate fragment
 - can be used to test equality.
    * must be equal to match?

MoveToConcl, MinusOne, MultiMember
  - force hyp order
  - preclude optimal layering
     * layer optimally but adjust at use? or after the fact.
       only relevant for hypnum permutation?

Alpha : 

alpha_thin_match -
   - returns name association
   - first arg is pattern,
   - ignores extraneous hyps in second arg.

these are very similar?:
 - match_alpha_generalized_iinf_sequent
 - match_alpha_normal_iinf_sequent_wthin



normalized to normalized (layered)  : for checking normalization, for inserting
  - no thinning
  - equal : no hypnum permutation
  - match : find hypnum permuation after matching vars. 

normalized to instance
  - match : do complete match, ie include reflexive renaming 
  - thinning : compute from var permutation, anything not included is thinned 
  - equal : are they equal if instance has extra hyps? can be made equal!



 ⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t

⋅

Home