type theory
Apr. 9th, 2008 11:42 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslI really sympathize with type theory folks' (or, at least jcreed's) desire for using type theory in common discourse. After Risi Kondor's lecture today, type theory made it possible for us to communicate formally and efficiently.
For example, the Fourier Transform on permutation groups
^ : (Perm -> Reals) -> (Repr -> Reals)
which is analogous to the regular FT
^ : (Time -> Reals) -> (Frequency -> Reals)
the function f : Graph x Perm -> {0,1} encodes whether there is an edge between the last two nodes in the permutation.
I want some sort of editor for helping me formalize natural language statements of a technical nature. Such formalization seems like a very good exercise when you're not familiar with the ideas and you're trying to see how they fit together. Still, I'm not sure exactly what features I'd want it for. Type inference (e.g.: SOLVED! "Blicket" is an instance of "Vehicle")? Catching fallacious or ill-formed statements? Automatic metonymy detection?
jcreed's) desire for using type theory in common discourse. After Risi Kondor's lecture today, type theory made it possible for us to communicate formally and efficiently.For example, the Fourier Transform on permutation groups
^ : (Perm -> Reals) -> (Repr -> Reals)
which is analogous to the regular FT
^ : (Time -> Reals) -> (Frequency -> Reals)
the function f : Graph x Perm -> {0,1} encodes whether there is an edge between the last two nodes in the permutation.
I want some sort of editor for helping me formalize natural language statements of a technical nature. Such formalization seems like a very good exercise when you're not familiar with the ideas and you're trying to see how they fit together. Still, I'm not sure exactly what features I'd want it for. Type inference (e.g.: SOLVED! "Blicket" is an instance of "Vehicle")? Catching fallacious or ill-formed statements? Automatic metonymy detection?