Xah Programing Blog Archive 2016-02

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

Unicode Hand Gestures 👍 👌 ✋

Unicode 7 New Characters

Wolfram Language Slow?