Ograničenje na slobodne varijable

> U TS skripti u odjeljku "Pokrate i proširenja jezika", zašto u "postoji jedinstven x phi", tj. u onome za što je to pokrata, tražimo da y ne bude slobodna u phi?

Uzmite φ:=(𝒙∈𝒚). Tada biste očito htjeli da ψ:=∃!𝒙φ znači "𝒚 je jednočlan", a jednočlani skupovi postoje, pa to nije univerzalno lažna tvrdnja.

No ako biste to raspisali kao ∃𝒚∀𝒙(𝒙=𝒚↔φ), relativno se lako vidi da to jest univerzalno lažna tvrdnja (dokažite za vježbu). Dakle nije ekvivalentna onom što smo htjeli formalizirati.

To je skroz formalni odgovor, koji Vas možda zadovoljava a možda i ne -- možda mislite da samo treba malo drugačije sintaksno iskazati tu pokratu, i bit će u redu. To nije istina, i vidi se ovako: φ ima dvije slobodne varijable, 𝒙 i 𝒚. Ako vežete 𝒙 kvantifikatorom jedinstvene egzistencije, i dalje varijabla 𝒚 mora ostati slobodna. Dakle formula ψ "ovisi" o 𝒚, u smislu da govori o nekom konkretnom objektu označenom varijablom 𝒚. No ovaj raspis o kojem govorimo veže varijablu 𝒚, pa ne "ovisi" o konkretnom 𝒚.

Postoje samo dva načina kako to možemo razriješiti. Jedan je da ne vežemo nijednu varijablu osim 𝒙 u raspisu, no kako očito moramo govoriti o dvomjesnoj relaciji jednakosti, nije jasno kako to napraviti bez uvođenja nove varijable. To ne mora biti 𝒚, može biti recimo 𝒛 -- ali tada, ako je 𝒛 vezana, imamo isti problem s formulom 𝒙∈𝒛; a ako je slobodna u raspisu, odjednom raspis ovisi o nekom objektu o kojem pokrata uopće ne govori (imamo isti problem s druge strane).

Drugi način je da se pomirimo s tim da će raspis pored 𝒙 vezati još neku varijablu, recimo 𝒚, ali onda moramo zahtijevati da ta varijabla ne smije biti slobodna u φ, jer očito neće biti slobodna u pokrati.

Također, "𝒚 nije slobodna u φ" ne valja gledati kao na ograničenje na φ, već je bolje to gledati kao ograničenje na 𝒚. U smislu, nađemo neku varijablu koja se ne pojavljuje u φ, recimo (BSOMP) da je to 𝒚, i onda shvatimo ψ kao pokratu za formulu s tom varijablom. [To je osnovni razlog zašto zahtijevamo beskonačno mnogo varijabli -- sve što nam zapravo treba je da uvijek postoji "nova" varijabla koju možemo uzeti.]

Dakle, naravno da mi znamo i što znači ∃!𝒙(𝒙∈𝒚) [i naravno da zapravo nisam pazio na to ograničenje kasnije:], samo što stroga formalizacija toga zahtijeva suptilnije alate od ovih koje trenutno imamo.

Apsorpcija binomnih koeficijenata

> Jel bi mi mogao pojasniti Veljanov dokaz svojstva apsorpcije binomnih
> koeficijenata, mislim strana 66. u novoj knjizi. Iako mi je samo
> svojstvo kombinatorno jasno (bar se nadam - od n objekata mozemo
> izabrati r na n povrh r nacina ili prvo mozemo izabrati jednog na n
> nacina, a onda od preostalih n-1 jos na r-1 nacina. Buduci da poredak
> nije vazan, dobit cemo r istih odabira (jer smo prvo mogli izabrati
> prvi, pa drugi, .. pa r-ti), pa jos podijelimo sa r i to je to.
>
> On uspostavlja neku fantomsku bijekciju za koju tvrdi da stima, a ja
> bih htio razumjeti i formalno matematicki dokaz jer ipak treba znati
> na taj nacin razmisljati.

Pa... treba se znati tako izražavati, jer si onda siguran da je ono što intuitivno misliš istina. No naravno da je stvar zapravo ovo što si ti opisao, samo preciznije. :-)

Dakle, prvo što treba razjasniti je da u kombinatornim interpretacijama nema razlomaka -- bar ne onih netrivijalnih. :-) Dakle, da bi dokazao (n#r)=n/r*(n-1#r-1) , ide prvo to pretvoriti u manifestno prirodne brojeve, kako bi znao to interpretirati kao kardinalne brojeve nekih skupova (npr. desna strana bi mogla značiti Kartezijev produkt, ali prvi faktor mu očito ne može imati n/r elemenata, ako r(!|)n ).

So, pomnoži s r i dobije r*(n#r)=n*(n-1#r-1) . Sad može obje strane jednakosti interpretirati kao kardinalnosti konačnih skupova, preciznije Kartezijevih produkata. Što je na lijevoj strani? Uređeni parovi (a, A), gdje je A@([n]#r) te a@A. Drugim riječima, broji r-člane podskupove od [n], svaki skupa s nekim njegovim istaknutim elementom.

Što je na desnoj strani? Uređeni parovi (b, B), gdje je (na prvi pogled) B@([n-1]#r-1) te b@[n]. No ovaj [n-1] je malo šašav... zašto bismo izbacivali baš n iz [n]? Puno je bolje izbaciti neki koji već imamo, konkretno b. (Primijeti da je i na lijevoj strani veza između a i A, samo je tamo pozitivna a@A. Ovdje je negativna b(!@)B.) Dakle, zapravo, na desnoj strani brojimo (b, B) takve da je b@[n] i B@([n]\{b}#r-1).

Sad stvarno nije teško vidjeti bijekciju. Ako ti netko da (a, A), gdje A ima r elemenata među kojima je a, ti vratiš (a, A\{a}) -- to je očito par kojem drugi član ima r-1 elemenata među kojima nije prvi član (a). U suprotnom smjeru, ako ti netko da (b, B) gdje B ima r-1 elemenata među kojima nije b, vratiš (b, BU{b}) -- i to je očito na lijevoj strani.

Ta dva preslikavanja su jedno drugom inverzi (ako ubaciš b pa ga izbaciš, dobit ćeš isto ako b nije bio na početku unutra, a isto tako ako izbaciš a koji jest unutra pa ga vratiš, dobit ćeš isto), pa su bijekcije odnosno broj elemenata lijevog skupa jednak je broju elemenata desnog. Kved.

Dynamic vs static typing

(This is a response to a post "Dynamic Languages are Static Languages". I tried to post a comment, but Wordpress told me it couldn't send it, probably because the post in question is too old. So I'm putting it here.)

Your thesis sounds wrong to me. My experience is that strong typing simply disallows some perfectly normal easy programs to be written. And that shouldn't be true if dynamically typed languages are just a special case of statically typed ones.

A few months ago, in order to learn Haskell (in an academic setting), I tried to write a Haskell function to test if a Boolean function was valid (always true). The literature I was using (The Haskell Road to Logic, Math and Programming, by Doets and van Eijck) did that in stages, valid1 for unary functions, valid2 for binary ones... I, as a diligent professional programmer, saw a common bit of code in those, and naively thought I could use recursion (and currying) to make a function valid, so that valid 1 was valid1, valid 2 was valid2, and so on. That way, my code would be much more general, _and_ easier to write.

Imagine my shock when I got an occurs check error. Of course, the problem is that valid1 had type (Bool->Bool)->Bool, but valid2 had type (Bool->Bool->Bool)->Bool, so there simply was no way for valid to have a type, and the GHC told me so. In fact, to be completely honest, valid _has_ a type: a dependent product type, n:Integer->(Bool->...->Bool)->Bool, where there are n arrows inside parentheses. But Haskell can't represent such types, at least as far as I learned (please correct me if I'm wrong).

So, you'll probably tell me I was simply using too weak a type system. But Haskell is the poster child for functional programming. If I can't use that, then what? Miranda is even weaker. Standard ML is not pure, it seems. Coq is not even Turing complete. _Where_ do you find that ideal typing engine you're constantly talking about? Or is it just a platonic ideal, with no implementations in the real world?

Or you're going to tell me that valid function is simply not a function. It is a nonsensical notion, since in a well-typed language you could only have valid1, valid2 and so on. To that I'll tell you it's nonsense. I have perfectly well represented valid in Coq, and Coq surely knows its type theory (however, as I said, it has other problems).

Or you're going to tell me that it's no better in the world of dynamically typed languages. That's simply not true. I can write valid in Python in a few minutes. (Thanks to Python's introspection capabilities, I can even drop the first parameter, and ask my argument function how many bools it would like to receive. But I know static typing fans would probably scream at such an idea.:)

Or you're going to tell me to shut up and simply use lists. Integer->([Bool]->Bool)->Bool is a good approximation, and I did use that variation in the end. But it feels like a horrible kludge. I don't want lists, at least I surely don't want Haskell's interpretation of them as codata. It makes no sense to ask if a Boolean function receiving an infinite list of arguments is valid. And even if it did, I have no way to put something in the "Integer" place. Yes, I can get rid of it, and get it from the length of the list. But the situation is even worse than that: I seem to have no way of restricting the argument to only receive lists with _same_ length. Boolean function that knows how to handle both 2-element and 3-element lists is simply not a valid argument for the function valid I was intended to write.

I don't think I can change your opinion, you obviously know a lot about those things. But maybe you can change mine, by communicating your idea better. What am I missing?