Xah Programing Blog 2016-01
Homotopy Type Theory
Linux: Move File to Trash by Command
Formal Definition of Systematic Grammar
1 xah's edu corner extempore. on what's computation of types?
2 the computation of types, and what's the nature of numerical computation? string computation? symbolic computation?
3 in haskell, ocaml, they have type inference. And it seems, computation of types can become a thing of itself.
4 as primary goal, as in some math proof system.
5 now, what's “computation of types”? what's its nature?
7 golang has type inference, but i think nothing close to haskell/ocaml in proof world.
8 so, what exactly is computation of types? if it exist? what's its nature?
9 to understand that, we look at something we know. For example, there's numerical computation, string computation, symbolic computation.
10 numerical computation is like 2+5, or find earth position, matrix, statistics, calculus, civil engineering, physics simulation, …
11 strings computation, or text processing, we also familiar. Any grep, regex, find/replace, report, extraction. We do everyday.
11.5 search engines, in large part, is string computation, text processing.
12 symbolic computation, typically derivative, integration, symbolic solution to equations. e.g. Wolfram Language Mathematica.
13 ok, we intuitively/practically understand numerical, string, symbolic computation. But, how can we explain them in terms of computation?
14 let's look at algorithms. there's algorithm for sort, for implement regex, for solving equation, traveling salesman problem.
14.5 what is THEIR difference? how to characterize their difference?
15 seems, they are simply different “problems”, or “problem domains”.
16 now, what does “problem” mean here? how can we explain it in terms of “computation”?
17 looks like we now need to look into the meaning of “computation”.
18 computation, most of the time have a goal. Human activated computation. e.g. we compute to solve a problem, or a do something, a goal.
19 as opposed to, nature's computation. As in, which rain drop on window will fall first.
19.5 Or, any thing in universe is computation of physical forces or perhaps some quantum. The churning of the universe.
20 so, human activated computation, come with a goal, or problem, to begin with.
21 now, problems comes in many forms, kinds. Math questions, academic questions, but also tasks, counting, processing, sorting.
22 so，if computation is using some machinary to automate some process… but still，how does this explain string/numerical/symbolic computation?
23 seems the question of string/numerical/symbolic computation is similar to asking what's diff of different algorithms, or problems.
24 e.g. what's the diff between, say, problems of algebraic geometry, vs diff equations, vs linear programing? or combinatorics problem?
25 so far, i don't have good answer. So, on the question of nature of the computation of types… i have no answer.
26 maybe you have an answer. suggest away.
for now, enjoy the most beautiful melody in history. Schubert Impromptu in G Flat 📺 http://xahmusic.org/piano/schubert_impromptu_G_flat.html
Hand Emoji 👍
Unicode 7 New Characters
Wolfram Language Slow?
- 1 many benchmarking/speed website, show Wolfram Language as slow, eg #julia. that's bullshit.
- 2 Wolfram Language has most commonly used algorithms as builtin functions, 8 thousand of them. Try compare one of those.
On Constructed Languages, Computer Languages, and Their Grammar Complexity
Why Does Struct Datatype Encroach Namespace?
Download Free Unicode Fonts
Jargon Automata in Finite State Automata
Python Tutorial now has navigation panel on the side.
Unicode Search 😄. now there's nav panel on the left side for each page.
Unicode Character in Variable/Function Names
- Problems of Symbol Congestion in Computer Languages; ASCII Jam vs Unicode
- Unicode in Function Names and Operator Symbol
Lisp notation isn't “prefix”
naming, terminalogy, are critical, because misnomer creates perpetual misunderstanding. Jargons of Software Industry
Formal logic's Chinese roots. Chinese, The Logicians or School of Names (名家)
Linux: LXDE/OpenBox, Disable Mouse Scroll Wheel Shade Window
City Hunter keyboard
a very strange keyboard, but seems real.
more screenshots, see City Hunter Keyboard
the term “ambiguous grammar” is a misnomer. Grammar of comp lang are never ambiguous. It should be called multi-parse-tree grammar
Linux: Make Scrollbar Always Visible
Regular Grammar, Lexical Grammar, Systematic Syntax, Uniform Syntax
for a decade, i wanted a term to describe certain syntax that's regular, such as a idealized lisp, XML, or Wolfram Language syntax.
I've used “regular grammar” and “lexical grammar”, but that's wrong. Perhaps systematic syntax or uniform syntax.
the Common Lispers, at times claim lisp syntax is simple by the idiotic phrase “no syntax”, at other times says lisp syntax can't described by grammar because of lisp reader. LOL
Jargons of Software Industry (updated.)
What's Closure in Programing Language (updated)
Python Doc Links All Dead
unix “grep” name, came from qed/ed editor command
g/re/p meaning “Global search for Regular Expression and Print matching lines”
Linux: How to Set Mouse Speed
Linux: How to Swap Mouse Buttons (updated)
W3C and WHATWG Dead URL
Valve Steam Controller. New device, novel design.
Why is Array Access Constant Time
What's Ontology of Programing Language?
CM Storm QuickFire Rapid-i keyboard. New from Cooler Master. Features a lighting effect with 32-bit ARM processor for effects