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?

6 of language i know of, perl python ruby JavaScript elisp clojure java golang, only last 2 has types.

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?

On Constructed Languages, Computer Languages, and Their Grammar Complexity

Why Does Struct Datatype Encroach Namespace?

Download Free Unicode Fonts

The Jargon Automata in Finite State Automata

Python Tutorial now has navigation panel on the side.

Unicode Characters ∑ ♥ 😄. now there's nav panel on the left side for each page.

Unicode Character in Variable/Function Names

minor update.

Lisp notation isn't “prefix”

math notation prefix infix postfix matchfix
math notation: prefix infix postfix matchfix

Concepts and Confusions of Prefix, Infix, Postfix and Lisp Notations

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.

City Hunter keyboard 00008
keyboard from 〈City Hunter 3〉 episode 9.

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 Languages? (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)


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

If you have a question, put $5 at patreon and message me.