pie#2 - specifying syntax

File: 12083946_1012986602056231_682349838_n.jpg (31KB, 720x960px) Image search: [Google]

31KB, 720x960px

== Example ==

So for example, if \mathrm {Type } is the most generic type in our system, and we want a theory with the rule that if \sigma and \tau are of type \mathrm {Type }, that then the symbols \sigma \to \tau and \sigma \times \tau also denote types, then we write this is

\frac { \sigma: \mathrm {Type } \ \ \ \ \ \ \ \tau: \mathrm {Type } } { \sigma \to \tau: \mathrm {Type } }

and

\frac { \sigma: \mathrm {Type } \ \ \ \ \ \ \ \tau: \mathrm {Type } } { \sigma \times \tau: \mathrm {Type } }

A merit of this formalization is that makes it hard to end up with wrong expression syntax like ' \land \land P'. We can use typing systems to define syntax for computer programs, or logic, of cookie recipes. For example, if P and Q are propositions and \land means "and", then we could introduce a type of propositions \mathrm {Prop } and formally express a rule how to form more propositions using these symbols:

\frac {P: \mathrm {Prop } \ \ \ \ \ \ \ Q: \mathrm {Prop } } {P \land Q: \mathrm {Prop } }

* Often, we study sequents expressing "Within the type declarations \Gamma (called context) from \Theta we can form \Psi" and this is written \Gamma| \Theta \vdash \Psi. Theta can be any formula and if we don't need any other formula than such a typing judgment \Gamma=x: \sigma, then we just have \Gamma \vdash \Psi.

File: 12067214_1012986558722902_2030323995_n-2.jpg (118KB, 720x960px) Image search: [Google]

118KB, 720x960px

== More examples ==

The following certainly give sensible expression in arithmetic:

\frac {n: {\mathbb {N } } \ \ \ \ \ \ \ m: {\mathbb {N } } } {n \cdot m: {\mathbb {N } } }

\frac {n: {\mathbb {N }} } {n+1: {\mathbb {N }} }

Or consider

\frac {A=B: \mathrm {Prop } } {B=A: \mathrm {Prop } }

Note, again, that the above is about what constitutes as syntactically correct expression in a logic, while e.g. the statement (A=B) \Rightarrow (A=B) is a statement within the logic itself. Indeed, we will have

\left((A=B) \Rightarrow (A=B) \right): \mathrm {Prop }.

== Even more examples ==

Here is an example for a derivation rule in proof theory. It expresses that if p is a proof for the proposition A \Rightarrow B and if x is a proof for the proposition A, then we can proof that B holds - and this proof is denoted by p \,x

\frac {p:(A \Rightarrow B) \ \ \ \ \ \ \ x:A } {p \,x:B }

Here is an example from category theory.
The following rule expresses that if g is an arrow in the Hom-class { \bf C }[A,B], and if f is an arrow in the Hom-class { \bf C }[B,C], then f \circ g is an arrow in the Hom-class { \bf C }[A,C].
\frac {g: { \bf C }[A,B] \ \ \ \ \ \ \ f: { \bf C }[B,C] } {f \circ g: { \bf C }[A,C] }

Here is an example of the theory //simply type lambda calculus//.
The following rule expresses that if f is a function from D in C, then for all x in D, then f applied to x is in C:
\frac {f:(D \to C) \ \ \ \ \ \ \ x:D } {f \,x:C }

File: IMG_2843.jpg (693KB, 3264x2448px) Image search: [Google]

693KB, 3264x2448px

Or more formally still, the following assumes that from a context \Gamma we can define spaces D and C and D \to C and the first two are indeed viewed as domain and codomain.
\frac { \Gamma \vdash f:(D \to C) \ \ \ \ \ \ \ \Gamma \vdash x:D } { \Gamma \vdash f \ x:C }

Remarks (no need to read):

There are type theory with types and terms completely separated. If we let types have a type (like in the example with \mathrm {Type } above), then types are also terms. If types functionally vary over terms we call the system dependently types and if the types vary over other types we have polymorphic types.

The most heavily studied type systems are those for computation. If you define the type former \to and the associated term constructor (lambda-terms) and rewriting rules, you soon get a Turing complete system.

The first lambda-calculus was untyped (just ad hoc constructors for terms) and this can be seen as simple type theory with the requirement ( \sigma \to \sigma) = \sigma.

The first thing one naturally adds after function types are product types \times and unit type 1. This lets you form lists and choose element. The natural categorical model is a
http://en.wikipedia.org/wiki/Cartesian_closed_category.

And then you might add sum types + and the empty type 0.
This way you can merge types and code if-statements.

Old thread:
>>7579704

>>7585026
That's a big shoe

Also, bumping based anon's thread

File: #Landau week 2.jpg (68KB, 640x426px) Image search: [Google]

68KB, 640x426px

>>7585060
for her

So my current plan is to post the logical derivation rules this week (starting constructively) but not to dwell on How To Prove It techniques and further derivation rules (that can be derived from the initial ones).

I'ma comment on Peano axioms then, then lambda calculus and natural numbers there, and then do the set theory axioms.
So maybe we do the empty set 10 days from there, rudimentary constructions, and then basic categories.

More discussions are encouraged. There were some relevant notes on Curry-Howard correspondence at the end of last week - note that above I purposely chose examples of concepts in different theories, which actually are the same concept in a topos
- Cartesian product, multiplication, logical "and"
- function space, exponentiation, implication

Does anybody know interesting or inovative programming languages being developed or significantly extended right now?

>>7585390
not a real answer, but fun
https://esolangs.org/wiki/Language_list

>>7585075
how old are you ?
what do you study at your university ?

There is one fully funded PhD studentship available (for EU citizens) in Nottingham with me as a supervisor. The studentship is related to a grant on Homotopy Type Theory supported by the UK EPSRC jointly with Nicola Gambino in Leeds and Neil Ghani and Conor McBride at the University of Strathclyde in Glasgow.

File: 1423350521618.jpg (73KB, 1600x1200px) Image search: [Google]

73KB, 1600x1200px

Review of our book by Julio Rubio.
Julio (https://esus.unirioja.es/psycotrip/) is an expert on computable
algebraic topology and one of the main implementors of the Kenzo
system.

http://www.ams.org/mathscinet/search/publdoc.html?pg1=INDI&s1=1063327&yrop=eq&dr=pubyear&arg3=2013


https://groups.google.com/forum/#!topic/homotopytypetheory/3TpQSTI_EdI


here is a course on constructive type theory as well as category theory
http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html

https://www.youtube.com/playlist?list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf

>>7586567
>http://www.ams.org/mathscinet/search/publdoc.html?pg1=INDI&s1=1063327&yrop=eq&dr=pubyear&arg3=2013
This page requires authentication to access.

I watched the first few of Awodey's lectures. They were pretty good though I'm actually in a Category Theory course at the moment so there was too much repeated material for me to continue watching them. Still I recommend them to other people. Also, I personally prefer his actual Category Theory book over the notes he supplies on that site (I've been using them to supplement my own instructor's Category Theory notes).

>>7585075
I'm the guy who was asking about the Curry Howard stuff at the end of last week (a few days ago). I'm still working my way through the material but some of it has been pretty helpful. The clarification on Haskell's "types and kinds" type system has helped me put into words what I'd been thinking all along.

I just wanted to thank you for keeping this up. I'll likely pop in throughout the week as I get time to study (I have a full courseload that really eats into my study time).

>>7585390
Theorem provers like Agda and such are programming languages but I suspect that's not what you're asking about.

You may want to look at Rust and Go. Both claim to be systems programming languages but they define that term differently. Rust is aimed at really fast low level programming (basically aims to replace C++), while Go is aimed at slightly higher level but still pretty serious software (basically aims to replace Java while also doing a bunch of concurrent server software stuff).

File: mehhl.png (413KB, 470x590px) Image search: [Google]

413KB, 470x590px

new thread
>>7586878

>>7586514
28, Aerospace engineering on paper, Physics at heart

>>7586668
So you read Adwodeys book? At least the start? Then you know much more than I thought anyway. What do you know?

The irc channels haskell and (for more theory) haskell-blah should be helpful for the kind stuff. I know there is one guy in particular (not on the irc, though), who is pushing kind games. And generally, I feel there is a feel to go dependent types with the haskell language.