Neinterpretovaná funkce - Uninterpreted function

V matematické logice je neinterpretovanou funkcí nebo symbolem funkce takový, který nemá žádnou jinou vlastnost než svůj název a n-ary formu. Funkční symboly se používají společně s konstantami a proměnnými k vytváření termínů .

Teorie uninterpreted funkcí je také někdy nazýván volný teorii , protože je volně generován, a tedy bez objekt , nebo prázdná teorie , být teorie má prázdnou množinu vět (analogicky k počáteční algebry ). Teorie s neprázdnou množinou rovnic jsou známé jako teorie rovnic . Problém uspokojivosti pro volné teorie je vyřešen syntaktickým sjednocením ; Algoritmy pro posledně jmenované používají tlumočníci pro různé počítačové jazyky, například Prolog . Syntaktické sjednocení se také používá v algoritmech pro problém uspokojivosti u některých dalších rovnicových teorií, viz E-sjednocení a zúžení .

Příklad

Jako příklad neinterpretovaných funkcí pro SMT-LIB, pokud je tento vstup zadán řešiči SMT : 

(declare-fun f (Int) Int)
(assert (= (f 10) 1))

Řešitel SMT by vrátil „Tento vstup je uspokojivý“. Stává se to proto, že f jde o neinterpretovanou funkci (tj. Vše, o čem je známo, f je její podpis ), takže je možné, že f(10) = 1 . Ale použitím níže uvedeného vstupu: 

(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))

Řešitel SMT vrátí „Tento vstup je neuspokojivý“. Stává se to proto, že ačkoli f nemá žádnou interpretaci, ale je nemožné, aby vracela různé hodnoty pro stejný vstup.

Diskuse

Rozhodovací problém pro volné teorií je obzvláště důležité, protože mnoho teorií může být snížena tím.

Volné teorie lze vyřešit hledáním běžných dílčích výrazů pro vytvoření uzavření kongruence . Řešitelé zahrnují řešitele modulárních teorií uspokojivosti .

Viz také

Poznámky

Reference


Ikona pahýl

Tento článek týkající se formálních metod je útržek . Wikipedii můžete pomoci rozšířením .