База — формальные доказательства:
- https://leanprover.github.io/logic_and_proof/
- https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
База — математика:
- «Конкретная математика. Основание информатики» (Д. Кнут)
suhr
/ US-Russian.keymap
Created
September 3, 2024 14:02
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/bin/keymap -l | |
| # | |
| # Raw key numbering for 101 keyboard... | |
| # [sys] [brk] | |
| # 0x7e 0x7f | |
| # [esc] [ f1] [ f2] [ f3] [ f4] [ f5] [ f6] [ f7] [ f8] [ f9] [f10] [f11] [f12] [prn] [scr] [pau] | |
| # 0x01 0x02 0x03 0x04 0x05 0x06 0x07 0x08 0x09 0x0a 0x0b 0x0c 0x0d 0x0e 0x0f 0x10 K E Y P A D K E Y S | |
| # | |
| # [ ` ] [ 1 ] [ 2 ] [ 3 ] [ 4 ] [ 5 ] [ 6 ] [ 7 ] [ 8 ] [ 9 ] [ 0 ] [ - ] [ = ] [bck] [ins] [hme] [pup] [num] [ / ] [ * ] [ - ] | |
| # 0x11 0x12 0x13 0x14 0x15 0x16 0x17 0x18 0x19 0x1a 0x1b 0x1c 0x1d 0x1e 0x1f 0x20 0x21 0x22 0x23 0x24 0x25 |
suhr
/ haiku.patch
Created
February 1, 2024 00:27
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a/platforms/unix/plugins/SocketPlugin/sqUnixSocket.c b/platforms/unix/plugins/SocketPlugin/sqUnixSocket.c | |
| index df8a1eec0..22f3cae87 100644 | |
| --- a/platforms/unix/plugins/SocketPlugin/sqUnixSocket.c | |
| +++ b/platforms/unix/plugins/SocketPlugin/sqUnixSocket.c | |
| @@ -57,6 +57,10 @@ | |
| #endif | |
| #endif | |
| +#ifdef __HAIKU__ | |
| +#define IFF_RUNNING IFF_LINK |
suhr
/ without_version.yaml
Created
December 22, 2023 02:55
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| - package: legacyPackages.x86_64-linux.addDriverRunpath | |
| pname: add-driver-runpath | |
| - package: legacyPackages.x86_64-linux.addOpenGLRunpath | |
| pname: add-opengl-runpath | |
| - package: legacyPackages.x86_64-linux.alacritty-theme | |
| pname: alacritty-theme | |
| - package: legacyPackages.x86_64-linux.all-cabal-hashes | |
| pname: all-cabal-hashes-def4ad9.tar.gz | |
| - package: legacyPackages.x86_64-linux.alsa-plugins-wrapper | |
| pname: ap64 |
suhr
/ reasoning.md
Created
June 19, 2023 09:06
suhr
/ llm-schizophasia.md
Created
March 21, 2023 15:02
I've done a curious little experiment on abnormal psychology applied to language models.
This is a textbook example of schizophasia in Russian:
Родился на улице Герцена, в гастрономе номер двадцать два. Известный экономист, по призванию своему — библиотекарь. В народе — колхозник. В магазине — продавец. В экономике, так сказать, необходим. Это, так сказать, система… э-э-э… в составе ста двадцати единиц. Фотографируете Мурманский полуостров и получаете «Те-ле-фун-кен». И бухгалтер работает по другой линии — по линии библиотекаря. Потому что не воздух будет, академик будет! Ну вот можно сфотографировать Мурманский полуостров. Можно стать воздушным асом. Можно стать воздушной планетой. И будешь уверен, что эту планету примут по учебнику. Значит, на пользу физике пойдёт одна планета. Величина, оторванная в область дипломатии, даёт свои колебания на всю дипломатию. А Илья Муромец даёт колебания только на семью на свою. Спичка в библиотеке работает. В кинохронику ходят и зажигают в кинохронике большой лист. В биб
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Syntax | Name | Description | Example | Output | |
|---|---|---|---|---|---|
| +/x | Sum | Sum all value in x | +/1 2 3 4 5 | 15 | |
| -':x | Deltas | Pairwise differences in x | -':1 2 3 4 | 1 1 1 1 | |
| |+x | Rotate matrix | Rotate x counterclockwise | |+3 3#!9 | (2 5 8;1 4 7;0 3 6) | |
| x@<x | Sort | Sort x | {x@<x}@8 3 7 1 | 1 3 7 8 | |
| ?x,y | Set union | Unique elements from x and y | ?"abac","adob" | "abcdo" | |
| x^x^y | Intersection | Common elements from x and y | {?x^x^y}["abac";"adob"] | "aba" | |
| x|-x | Absolute value | Absolute value of x | {x|-x}@-1 | 1 | |
| */y#x | Power | x in power of y (y>0) | {*/y#x}[2;5] | 32 | |
| y@(#y)!x+!#y | Rotate left | Rotate y by x elements to the left | {y@(#y)!x+!#y}[3;"abcde"] | "deabc" |
We can make this file beautiful and searchable if this error is corrected: Illegal quoting in line 6.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| SYNTAX NAME DESCRIPTION EXAMPLE | |
| +/x Sum Sum all value in x +/1 2 3 4 5 → 15 | |
| -':x Deltas Pairwise differences in x -':1 2 3 4 → 1 1 1 1 | |
| |+x Rotate matrix Rotate x counterclockwise |+3 3#!9 → (2 5 8; 1 4 7;0 3 6) | |
| x@<x Sort Sort x {x@<x}@8 3 7 1 → 1 3 7 8 | |
| ?x,y Set Union Unique elements from x and y ?"abac","adob" → "abcdo" | |
| x^x^y Intersection Common elements from x and y {?x^x^y}["abac";"adob"] → "aba" | |
| x|-x Absolute value Absolute value of x {x|-x}@-1 → 1 | |
| */y#x Power x in power of y (y>0) {*/y#x}[2;5] → 32 | |
| y@(#y)!x+!#y Rotate left Rotate y by x elements to the left {y@(#y)!x+!#y}[3;"abcde"] → "deabc" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #![allow(unused, non_camel_case_types)] | |
| pub mod m | |
| { macro_rules! bE | |
| { ($c:expr; $t:expr; $e:expr) => (if $c {$t} else {$e}); | |
| ($c:expr; $t:expr; ) => (if $c {$t} else { }); | |
| ($c:expr; ; $e:expr) => (if $c { } else {$e}); } | |
| macro_rules! oE | |
| { ($o:expr; $x:pat,$s:expr; $n:expr) => (match $o {Some($x)=>$s, None=>$n}); | |
| ($o:expr; $x:pat,$s:expr; ) => (match $o {Some($x)=>$s, None=>()}); |
Let's reduce the operations on rank-1 arrays (lists) down to very basic functions.
Two views on lists:
- A list is a function from indices to values
- A list is a free monoid
The first view gives ↕n, i⊑x and x⊏y, which correspond to the identity function, application
and composition, and also gives f¨x and x f¨ y.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| s:+: FlipAdd :g | |
| s:-: NegateSubtract :g | |
| s:*: FirstMultiply :g | |
| s:%: SquareRootDivide :g | |
| s:!: EnumerateOdometerDictonaryKeysDivideModulo :g | |
| s:&: WhereDeepWhereAndMinimum :g | |
| s:|: ReverseOrMax :g | |
| s:<: OpenAscendLess :g | |
| s:>: CloseDescendMore :g | |
| s:=: GroupUnitMatrixEqual :g |
NewerOlder