Mali popravkec funkcije izbire za S pod naravnimi about funkcionali-izbire

[andrejbauer]

O čem je tu govora, ker se zdi precej sumljivo.

[Petkomat]

V 5. vrstici datoteke zapiski.txt vrneva 1. Vrniti pa morava neki element iz S, ker funkcija izbire izbira elemente iz S.
(Ker denes v prvih 15h sekundah nisva našla načina, kako odpreti issue tik ob datoteki ipd, sva ga pač samo odprla kot opozorilo, kaj morava popraviti.)

[andrejbauer]

A je vseeno, kateri element, samo da je en element iz S? V tem primeru je najbolje, če definirata type class Pointed:

class Pointed t where
    point :: t

Potem enostavno vrneta point. Seveda je treba tudi definirati instance, recimo:

instance Num t => Pointed t where
    point = 0

instance Pointed () where
    point = ()

instance (Pointed a, Pointed b) => Pointed (a, b) where
    point = (point, point)

instance Pointed b -> Pointed (a -> b) where
    point = \_ => point

in tako naprej (na pamet pišem kodo, tako da verjetno ne deluje).

[Petkomat]

Hm. Videti je, kot da je vrednost point določena že s tipom? Če je tako, potem to ni ok, ker mora biti element, ki ga vrneva, v množici S, ta pa je zgolj podmnožica v množici Nat oz. v Nat -> Nat oz. v (Nat -> Nat) -> Nat. Ker je tisti element povsem odvisen od množice, ga niti ne moreva definirati rekurzivno, kot je to storjeno zgoraj.

[andrejbauer]

Aha, ok. Izgleda, da ne vem, kaj se dogaja. A je poanta, da se izračuna element S, ali se bo vedno v naprej vedel neki element S?

[Petkomat]

Množica S je fiksna in neznana, imava eksistenčni kvantifikator zanjo, napisati morava pa funkcijo izbire. Ta dobi predikat p. Če v S obstaja kak element, ki zadošča temu predikatu, potem morava vrniti enega od teh, ki zadoščajo, sicer pa poljubnega iz S (to je ta, o katerem že vseskozi na pol govorimo).

Če v naprej izračunava neki element v S, privarčujeva čas za izračun nekega vsakič, ko bo p(S) = {False}. Drugih prednosti ni.

[andrejbauer]

Aha, potem pa predlagam, da vzameta element S kot input. Tak element je "dokaz", da S ni prazna množica (oz. da je naseljena).