ČTK (Česká tisková kancelář) upozorňuje (X), že na jejím zpravodajském webu České noviny byly dnes dopoledne neznámým útočníkem umístěny dva smyšlené texty, které nepocházejí z její produkce. Jde o text s titulkem „BIS zabránila pokusu o atentát na nově zvoleného slovenského prezidenta Petra Pelligriniho“ a o údajné mimořádné prohlášení ministra Lipavského k témuž. Tyto dezinformace byly útočníky zveřejněny i s příslušnými notifikacemi v mobilní aplikaci Českých novin. ČTK ve svém zpravodajském servisu žádnou informaci v tomto znění nevydala.
Byla založena nadace Open Home Foundation zastřešující více než 240 projektů, standardů, ovladačů a knihoven (Home Assistant, ESPHome, Zigpy, Piper, Improv Wi-Fi, Wyoming, …) pro otevřenou chytrou domácnost s důrazem na soukromí, možnost výběru a udržitelnost.
Společnost Meta otevírá svůj operační systém Meta Horizon OS pro headsety pro virtuální a rozšířenou realitu. Vedle Meta Quest se bude používat i v připravovaných headsetech od Asusu a Lenova.
Společnost Espressif (ESP8266, ESP32, …) získala většinový podíl ve společnosti M5Stack, čímž posiluje ekosystém AIoT.
Byla vydána nová stabilní verze 3.5 svobodného multiplatformního softwaru pro editování a nahrávání zvukových souborů Audacity (Wikipedie). Přehled novinek také na YouTube. Nově lze využívat cloud (audio.com). Ke stažení je oficiální AppImage. Zatím starší verze Audacity lze instalovat také z Flathubu a Snapcraftu.
50 let operačního systému CP/M, článek na webu Computer History Museum věnovaný operačnímu systému CP/M. Gary Kildall z Digital Research jej vytvořil v roce 1974.
Byl zveřejněn program a spuštěna registrace na letošní konferenci Prague PostgreSQL Developer Day, která se koná 4. a 5. června. Na programu jsou 4 workshopy a 8 přednášek na různá témata o PostgreSQL, od konfigurace a zálohování po využití pro AI a vector search. Stejně jako v předchozích letech se konference koná v prostorách FIT ČVUT v Praze.
Po 48 letech Zilog končí s výrobou 8bitového mikroprocesoru Zilog Z80 (Z84C00 Z80). Mikroprocesor byl uveden na trh v červenci 1976. Poslední objednávky jsou přijímány do 14. června [pdf].
Ještě letos vyjde Kingdom Come: Deliverance II (YouTube), pokračování počítačové hry Kingdom Come: Deliverance (Wikipedie, ProtonDB Gold).
Thunderbird 128, příští major verze naplánovaná na červenec, přijde s nativní podporou Exchange napsanou v Rustu.
17.2.2013 20:42
Bystroushaak | skóre: 36
| blog: Bystroushaakův blog
| Praha
Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
AbcLinuxu.cz
ITBiz.cz
HDmag.cz
AbcPráce.cz-- nejprve operator ekvivalence
(==) :: Eq a => a -> a -> Bool
-- nerovnost ?
(/=) ? Eq a => a -> a -> Bool
-- error: cannot infer
-- musi natukat clovek
x /= y == not (x == y)
-- a je to :)
x /= y = not (x == y)Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
Docela mě překvapuje, že to nevrátí třeba x /= y = True.
Příkaz Auto zvládne doplnit i složitější výrazy. Například return a bind pro stavovou monádu doplní takto:
record Pair (A B : Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B
record State (S A : Set) : Set where
constructor state
field
runState : S → Pair S A
-- vygenerovane prikazem Auto
return : {S A : Set} → A → State S A
return x = state (λ z → z , x)
-- vygenerovane prikazem Auto (a spatne)
bind : {S A B : Set} → State S A → (A → State S B) → State S B
bind m f = state
(λ z →
z ,
Pair.proj₂
(State.runState (f (Pair.proj₂ (State.runState m z))) z))
bind je bohužel špatně – typ totiž nezakazuje použití původního stavu. Když ale umožním, aby se typ stavu měnil (pak už to není monáda), tak Auto vygeneruje již korektní definici i pro bind:
record IState (S₁ S₂ A : Set) : Set where
constructor state
field
runState : S₁ → Pair S₂ A
-- vygenerovane prikazem Auto
ibind : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind m f = state
(λ z →
Pair.proj₁
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z)))
,
Pair.proj₂
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z))))
Nicméně perfektní to není – některé výrazy se tam zbytečně opakují, člověk by napsal:
-- napsane clovekem
ibind' : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind' m f = state
(λ st₁ →
let (st₂ , a) = IState.runState m st₁
in IState.runState (f a) st₂)
IMHO to ale moc prakticky neni.Hodí se to v důkazech. Tam potřebuji najít term s daným typem a už příliš nezáleží na tom, jak ten term vypadá.
18.2.2013 13:38
coder | skóre: 4
| blog: lINUKS
18.2.2013 21:00
Josef Kufner | skóre: 70
19.2.2013 15:28
coder | skóre: 4
| blog: lINUKS
Bez Vimu si jiz nedokazi predstavit svuj zivot 
Ale ten Emacs ma spousty zajimavych funkci a doplnku, ktere bych rad pouzival a ve svete vimu jsou nedokonale imitovane. Napr. org mod a velmi kvalitni integrace REPLu funkcionalnich jazyku. No uvidim, treba se nekdy hacknu.
Hm, moc tomu nerozumim
Máte nějaký konkrétní dotaz, třeba bych mohl pomoci?
Mně se na Agdě a podobných jazycích líbí minimalističnost kombinovaná se silou typového systému. Naopak mi vadí absence aktuální definice jazyka – bylo by super, kdyby někdo zpracoval definici na úrovni Standard ML (viz stará verze: The Definition of Standard ML - Version 2).
Hlavní využití příkazu Auto je při hledání důkazů – tam totiž jde pouze o nalezení termu s odpovídajícím typem a je jedno, jak ten term vypadá. Je tohle odpověď na vaši otázku?
int f(int a, int b)a editor me k tomu doplnil:
{
return a + b;
}
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
Přesně tak. Například, když chci odčítání a použiji typ
binop₁ : ℕ → ℕ → ℕ
tak dostanu
binop₁ a b = b
což není odčítání. Musím tedy upřesnit typ:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y)
Místo pouhého čísla vracím dvojici. První prvek dvojice je číslo a druhý prvek je důkaz, že první prvek je rozdíl x a y. Odečítání definuji následovně:
_∸_ : ℕ → ℕ → ℕ m ∸ zero = m zero ∸ _ = zero suc m ∸ suc n = m ∸ n
Rovnost vyjadřuji pomocí následujícího typu. Typ je navržen tak, že term refl typu a ≡ b jde zkonstruovat pouze tehdy, jsou-li a a b stejné:
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
Následuje definice závislého páru, kde typ druhé složky závisí na hodnotě první složky:
record Pair (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
Nastavení parseru:
infixl 6 _∸_ infix 4 _≡_ _,_
Funkce vracející typ (tj. výrok), že rozdíl prvních dvou čísel je roven třetímu číslu:
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = x ∸ y ≡ res
Pro tento typ už příkaz Auto vygeneruje požadovanou funkci:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y) binop₂ a b = a ∸ b , refl
24.2.2013 22:50
Josef Kufner | skóre: 70
Myslím, že neuniká. V ničem to není lepší. Je to jen příklad, že vlastnost výsledku funkce jde specifikovat typem. V tomto případě to však nemá žádné výhody – spíše naopak.
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.
25.2.2013 11:02
Josef Kufner | skóre: 70
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.Tohle větou jsi měl celý článek uvést
Vygenerovalo by to neco i kdybych nenadefinoval operator _-_ a minus_pred definoval jinym zpusobem - treba pomoci scitani?
Nejspíš ne.
Konkrétně, pokud máte na mysli podobnou definici
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = y + res ≡ x
tak ne. Problém je v tom, že pro x < y neexistuje přirozené číslo res a Auto hledá totální funkci (všude definovanou).
Kdybych zadefinoval relaci ≥ a funkci binop₂ definoval pouze pro x ≥ y, tak by to stejně nenašel – je to už příliš složité. Nezkoušel jsem to, ale myslím, že by se muselo nadefinovat ∸, pak dokázat lemma, že z x ≥ y a x ∸ y ≡ res plyne y + res ≡ x, a pak by to našel (ale to už není příliš zajímavé, protože je to vlastně celé hotové).
Tiskni
Sdílej:
