All entries

Generikus programozás

17 October 2008 (ELTE programming) (2 comments)

A héten Rinus Plasmeijer tartott vendégelőadást a generikus programozásról funkcionális nyelvekben, bemutatva a Clean azon nyelvi elemeit, amivel explicit szupportálja ezt. Encsé a lelkemre kötötte, hogy blogjam meg, miről is van szó.

Kiinduló "Hello World"-ként tekintsük az alábbi Haskell kódot, benne két, strukturális rekurzióval definiált ekvivalenciavizsgálatot listákra és fákra:

data List a ≔ Nil | Cons a (List a)
data Tree a b ≔ Leaf a | Branch b (Tree a b) (Tree a b)

instance (Eq a) ⇒ Eq (List a) where

Nil = Nil ≔ ↑
Cons x xs = Cons y ys ≔ x = y ∧ xs = ys
⊥ = ⊥ ≔ ↓

instance (Eq a, Eq b) ⇒ Eq (Tree a b) where

Leaf x = Leaf y ≔ x = y
Branch x xt1 xt2 = Branch y yt1 yt2 ≔ x = y ∧ xt1 = yt1 ∧ xt2 = yt2
⊥ = ⊥ ≔ ↓

Kellően messziről nézve a fenti két függvény láthatóan megegyezik. Az általános (mondhatnám, generikus) ötlet éppen az, hogy a strukturális rekurziót mint patternt nyelvi elemmé emeljük.

Hacktivity 2008

21 September 2008 (unix windows programming math) (7 comments)

Encsé hívta fel a figyelmemet, hogy most lesz az idei Hacktivity, amelyről ő már tavaly is tudósított. Átnéztem a programot, és cím alapján sok előadás igérkezett érdekesnek. Meg a hekkelős játékra is kiváncsi voltam.

Az előadások végül nagyon változó színvonalúak voltak: volt közte pár teljesen content-less (pl. az XSS-előadást ilyen szinten én is meg tudtam volna tartani úgy, hogy nem is értek hozzá), a kvantumkriptográfiai előadás egészen addig volt jó, amig ki nem derült, hogy az előadó nem érti a kérdésemet.

Volt viszont pár tényleg jó előadás is, ottvolt egy FPGA-val MD5-öt törő srác, állati érdekes volt az alacsonyszintű wifidriver-törés (buffer overrunt okozó AP advertising beacon csomagokkal), pedagógiailag nézve pedig a szivárványtáblás előadás vitte a prímet.

Ami meg a hekkelős wargame-et illeti, tavaly ugye le-DoSolták a pontszámokat nyilvántartó gépet, idén meg kb. félóránként tartottak amatőr félórat... Encsé kollégával együtt feszültünk neki a feladatoknak. Volt köztük egy-két vállalható, volt néhány, ami jópofa lett volna, csak sajnos általában nem működtek (az pl. elég jellemző volt az egészre, amikor odamentünk a rendezőkhöz a 10. feladathoz megszerzett jelszavunkkal hogy nem fogadja el a rendszer, erre kiderült hogy a kétszámjegyű feladatokhoz nem működik és kicsit még faragni kellett). Aztán volt egy pár SQL injection-ös, az nagyon nem az én világom, úgyhogy ezekkel Encsé próbálkozott.

Aztán persze az lett a dolog vége, hogy fölényesen megnyertük. Kaptunk egy Linksys wifi routert meg egy külső merevlemezt, majd holnap szétosztjuk. Viszont ami vicces volt, hogy utána odajöttek ketten is hogy elkérjék az email-címemet mindenféle ilyen hálózati biztonsági munkákkal, pedig baromira nem értek én ezekhez, meg kedvem sincs, el is hajtottam őket azzal, hogy én inkább programozó vagyok...

Viki in a nutshell

15 September 2008 (personal) (5 comments)

Vikiről röviden #1: a meta-táska. Vikinek van egy kicsi rózsaszín és egy nagyobb, kék táskája. Ma vettem észre, hogy a kékben főleg a rózsaszínt hordja. Mint elmondta, azért, mert bizonyos ruhákhoz nem megy a rózsaszín, átpakolni mindent meg milyen macera lenne.

Vikiről röviden #2. Múltkor látta rajtam a Menő Manós pólómat, és tökre tetszett neki. Most meg a TV-ben pont az ment, és erre úgy hívta fel a figyelmemet, hogy "a pólód van a TV-ben".

Programozás visszavezetéssel

4 September 2008 (ELTE programming) (4 comments)

Hát akkor nézzük, mivel is tervezek foglalkozni Fóthi Ákossal a hétfőn kezdődő félév során, progmatos nagyprogramom keretében.

Az alapötlet az, hogy gépi segítséggel bizonyítsunk programozási tételeket , visszavezetés segítségével, és az "ötleteket", az invenciózus lépéseket a felhasználó, ne pedig valamilyen hilbertiánus, féseggű MI-engine találja ki. Tehát a papírt-ceruzát váltanánk csak ki, a hibázás lehetőségét akarjuk csökkenteni és az eredmények menedzselhetőségét növelni.

A "Hello World" szintet például az jelenti majd, ha abból a tételből, hogy ismerjük tetszőleges f:ℤ→ℤ illetve β:ℤ→𝕃 függvények esetén az alábbi feladat (Hoare/Dijkstra/Fóthi értelemben) megoldását...

A:	(m: ℤ) × (n: ℤ) × (l: 𝕃) × (i: ℤ) × (max: ℤ)
B:	(m': ℤ) × (n': ℤ)
Q:	m=m' ∧ n=n' ∧ m≤n ∧ [m, n]⊆dom(f)
R:	Q ∧ l=(∃k∈[m,n]:β(k)) ∧ l⇒ (i∈[m,n] ∧ β(i) ∧ max=f(i) ∧ ∀k∈[m,n]:β(k)⇒f(k)≤max)

(egyrészt vegyük észre, hogy természetesen a feltételes maximumkeresésről van szó, másrészt gondolkodjunk el azon, milyen fun lehetett ezt egyenként, Unicode táblázatokat böngészve beírnom)

... be tudjuk látni, hogy akkor meg tudjuk oldani bármilyen, mondjuk g:ℤ→ℤ függvényre az egyszerű minimumkeresést is, vagyis az alábbi feladatot:

A:	(m: ℤ) × (n: ℤ) × (i: ℤ) × (min: ℤ)
B:	(m': ℤ) × (n': ℤ)
Q:	m=m' ∧ n=n' ∧ m≤n ∧ [m, n]⊆dom(g)
R:	Q ∧ i∈[m,n] ∧ min=g(i) ∧ ∀k∈[m,n]:g(k)≥min

Erre egyébként van már annyi szanaszét heverő Lisp kódrészletem, amennyiből valószínűleg össze lehetne kalapálni valamit, ami ennyit már épp majdnem tudna is. Stay tuned.

Geekparty és egy breaking news

17 August 2008 (personal ISC food) (3 comments)

Múlt héten, csütörtökre raktuk a lakásavató geekbulit az ISC-s kollegákkal. A terv az volt, hogy spagettit és Guitar Herot tolunk az arcunkba, mindkettőt nagyobb mennyiségben. Végül mindkettő sikerült is.

Elsőre mondjuk gigászi feladatnak tűnt egyedül főzni hat emberre, már csak azért is, mert teljesen ismeretlenek voltak számomra az arányok. Ennek megfelelően sikerült is egy egész kiló pasta-t kifőzni, aminek a fele sem fogyott persze el, ráadásul a visionary leader-ünk hatására a lé, amiben a tészta főtt, viszonylag egyenletesen beterítette a főzőlapot. Viszont mentségére legyen mondva, hogy beszerzőmissziót szervezett az Ikeába, ahonnan feltehetőleg Büdåppest márkájú sajtreszelőt zsákmányolva érkeztek (kiváncsi vagyok, hogy vezethetett Zape, ha azóta se Maya, se Encsé nem nagyon akar beülni mellé).