
META TOPICPARENT 
name="HfstHome" 
HFST: API for Generalized Restriction (GR) and Predicate Logic in FST Calculus 

OvertFstHandle 
connect_with_concatenation (OvertFstHande e, OvertFstHande f) 
Combines two overt FSTs under concatenation. 


OvertFstHandle 
connect_with_and (OvertFstHande e, OvertFstHande f) 
Combines two overt FSTs under conjunction. 


OvertFstHandle 
connect_with_relative_complement (OvertFstHande e, OvertFstHande f) 
Combine two overt FSTs as e ∪ ¬f . 




< < 
OvertFstHandle 
quantify_existentially (VarHandle m, OvertFstHandle φ) 
Restricts φ to those strings that contain an m and hides then m in φ , or computes (∃ x)φ(x) . 



> > 
OvertFstHandle 
quantify_existentially (VarHandle m, OvertFstHandle φ) 
Restricts φ to those strings that contain an m and hides then m in φ by removing them like epsilons, i.e. computes (∃ x)φ(x) . 


TransducerHandle 
quantify_existentially_all (OvertFstHande e) 
Removes all auxiliary symbols. 




OvertFstHandle 
quantify_universally (VarHandle m, OvertFstHandle φ) 
Restricts x to all substrings in φ by evaluating Σ^{*} <x> Σ^{*} <x> Σ^{*} =^{x}> φ i.e. computes ¬ ((∃ x) ¬φ(x)) that is the same as (∀ x)φ(m) . 




< < 
OvertFstHandle 
quantify_universally_all (OvertFstHandle φ) 
The essential part of the ordinary GR operation that removes all variables at once like repeatly applying quantify_universally for all of them. 



> > 
TransducerHandle 
quantify_universally_all (OvertFstHandle φ) 
The essential part of the ordinary GR operation that removes all variables at once like repeatly applying quantify_universally for all of them. 




Function Supporting Substring Variables 