Značky tt
a ff
jsou jednoduše symboly pro pravdivou a nepravdivou hodnotu. Další primitivní typ je třeba typ všech celých čísel Int
.
Z primitivních typů je možné pomocí operací vytvářet další, bohatší typy.
union
v C nebo Either
v Haskellu)
Další příklady jsou ve slidech z přednášky na straně 167.
Funkce f je monotonní právě tehdy, když platí ∀a, b : a ≤ b ⇒ f(a)≤f(b).
Tedy: funkce f je monotonní, pokud pro každé dva prvky jejího definičního oboru platí, že pokud je jeden méně definovaný než jiný, tak potom jejich obrazy na tom budou stejně.
Takže například funkce f je monotonní, ale funkce g monotonní není.
f () = True
f ⊥ = True
g () = True
g ⊥ = False
Spojitost funkce je ještě trochu silnější pojem. Každá spojitá funkce je i monotonní. Obrácené tvrzení neplatí, existují i nespojité monotonní funkce. Platí ale, že každá monotonní funkce s konečným definičním oborem (doménou) je spojitá2.
Funkce f je spojitá, pokud pro každý spočetný řetězec x1, x2, … platí f(⨆(x1, x2, …)) = ⨆(f(x1),f(x2),…)
(Značka ⨆ značí supremum, nejmenší horní závoru, least upper bound. Horní závora nějaké podmnožiny je prvek, který je větší než libovolný prvek dané podmnožiny.)
Definice tedy říká, že obraz suprema libovolného řetězce musí být supremem obrazů jednotlivých prvků řetězce.
Česky: pokud se vezme libovolný spočetný řetězec a funkcí f zobrazíme jeho supremum, tak musíme dostat totéž, jako kdybychom postupně zobrazili všechny prvky daného řetězce a našli supremum obrazů.
Zadání: Napište všechny spojité funkce typu Unit⊥ → Bool⊥. Co je to funkce s tímto typem? Takováto funkce musí každé hodnotě z Unit⊥ přiřadit něco z Bool⊥.
Tyto funkce by bylo vhodné taky seřadit do diagramu, aby bylo patrné, jak to uspořádání na nich funguje. Pro jednoduchost je každou funkci možné zakreslit jako diagram ve tvaru definičního oboru, kde se místo původních prvků na stejná místa doplní hodnota, na kterou se ten který prvek zobrazí.
Pro jiný typ funkcí to může dopadnout třeba tak, jako na obrázku níž.
Striktní funkce je taková funkce, která nejdříve vyhodnotí svůj argument a potom s ním teprve něco počítá. Pokud je tedy argument nedefinovaný, nemůže být definovaný ani výsledek výpočtu. Pro striktní funkci tedy platí f ⊥ = ⊥.
Pro každé j ≥ 1 existuje vyčíslitelná funkce Φ : Nj + 1 → N, která je univerzální pro standardní numeraci j-árních funkcí. Tedy pro každé e ∈ N a (a1, …aj)∈Nj platí
Pro každou aritu tedy existuje funkce Φ, která bere o jeden argument víc -- potřebuje ještě index programu, který má simulovat. Důkaz věty spočívá v definici interpretu -- programu, který bude simulovat jiné programy.
Ke každému n ≥ 1, m ≥ 1 existuje totálně vyčíslitelná funkce smn : Nm + 1 → N, taková, že platí
Takže: existuje funkce s, která pro index programu i a m jeho argumentů spočítá index jiného programu, který bude dělat totéž co i, ale bude potřebovat o m argumentů méně. Funkce s vlastně zafixuje prvních m argumentů na nějaké konstanty. m je tady počet fixovaných parametrů, n počet těch, které se nefixují.
Dokazuje se pomocí programu, který celou konstrukci realizuje -- má m konstant a přesypává argumenty tak, aby to sedělo. Prvních n argumentů posune o m pozic doprava a na uvolněná místa dosadí konstanty. Pozor, aby se při posunování nepřepsalo něco, co bude ještě potřeba.
Nechť I ⊂ N je netriviální (není prázdná ani se nerovná N) a rekurzivní. Potom existují indexy programů i ∈ I a j ∈ I′1 tak, že ϕi = ϕj.
Tedy pokud je netriviální podmnožina N rekurzivní, potom nerespektuje funkce a naopak pokud nějaká množina respektuje funkce a je netriviální, potom nemůže být rekurzivní.
Důkaz se provede sporem: předpokládejme, že množina respektuje funkce a že množina I obsahuje index nějaké vyčíslitelné funkce2 θ, která není prázdná. I′ potom obsahuje indexy prázdné funkce. Kdyby tomu tak nebylo, tak se prohodí I a I′.
Nechť Pf(i) je program begin
x2 :=
Φ(i, i);
x1 :=
θ(x1) end
. Zřejmě program P počítá funkci θ, pokud ϕi(i) je definované a jinak počítá prázdnou funkci.
Tedy pro všechna i ∈ N platí ϕf(i) = θ právě tehdy když i ∈ K.
Pokud tedy f(i)∈I, pak f(i) není index prázdné funkce. Je to index θ. Obráceně pokud f(i) je indexem funkce θ, pak f(i)∈I. Nechť χI je charakteristická funkce I. Pro všechna i ∈ N musí platit
Protože χI ∘ f je totálně vyčíslitelná, musela by K být rekurzivní, což zřejmě není.
Necht I ⊂ N respektuje funkce a nechť existuje funkce θ taková, že všechny její indexy jsou v I a má vyčíslitelné rozšíření θ′ takové, že jeho indexy patří do I′.
I potom není rekurzivně spočetná.
Důkaz půjde zase sporem. Nechť funkce ξ(i, j) se rovná θ′(j), pokud ϕi(i) je definováno a jinak se rovná θ(j). Tato funkce je vyčíslitelná3. Podle věty o parametrizaci existuje totálně vyčíslitelná funkce f : N → N taková, že ξ(i, j)=ϕf(i)(j). f(i) potom patří do I právě tehdy, když ϕi(i) není definováno. Tj. f(i)∈I ≡ i ∈ K′.
Pokud by tedy I byla rekurzivně spočetná, tak i K′ by musela být rekurzivně spočetná. To ale není.
Při použití druhé Riceovy věty je tedy zřejmě potřeba zvolit θ tak, aby nebyla totální. Jinak by totiž neměla potřebné rozšíření.
Nechť I ⊂ N respektuje funkce a nechť existuje funkce θ taková, že všechny její indexy patří do I a navíc všechna její konečná zúžení patří do I′.
I potom není rekurzivně spočetná.
Důkaz se opět provede sporem. Nechť funkce μ(i, j) počítá θ(j), pokud Pi nezastaví pro vstup i během nejvýše j kroků. Pokud zastaví během nejvýše j kroků, μ se zacyklí. Funkce μ je zřejmě vyčíslitelná.
Podle věty o parametrizaci existuje totálně vyčíslitelná funkce f tak, že μ(i, j)=ϕf(i)(j).
Dostaneme tedy, že pokud i ∈ K, tak Pi zastaví pro i. Tedy existuje j takové, že Pi zastaví pro i po přesně j krocích. Tj. existuje j takové, že ϕf(i)(x) počítá θ(x) pro všechna x menší než j a jinak je nedefinované. Potom ale ϕf(i) je zúžením θ a její definiční obor je konečný, tedy ϕf(i) ∈ I′.
Z druhé strany platí, že když i ∈ K′, tak Pi nikdy nezastaví a ϕf(i) počítá celou θ a tedy patří do I.
Tedy i ∈ K′≡f(i)∈I a I nemůže být rekurzivně spočetná.
Třetí Riceovu větu tedy zřejmě nejde použít, pokud I obsahuje prázdnou funkci. Ta je totiž konečným zúžením každé funkce.
Funkce f roste nejvýše tak rychle jako g.
∃c, n0 : ∀n ≥ n0 : f(n)≤cg(n)
Funkce f roste pomaleji než g
Funkce f roste alespoň tak rychle jako g