*rc3 hacc preroll music*
Herald: All right, we are back again from the HACC or about:future studios on the
rc3 remote Congress 3 this year sadly remote so we'll do as we can. We have a
really nice talk coming up here about type theory in linguistics and about meaning in
linguistics. From daherb. He will be talking about the uses of type theory in
both programing languages and natural languages and maybe draw, like,
similarities between them. He has a PhD in computer science, was in Sweden for 6 years
at a university and is now back in Germany. There is sadly no translation for
this talk because there aren't enough angels to do all the translation work.
There is a pixelflut behind me. It's my own implementation. So if you want to spam
me, you can. I'm not sure if it will work, but apart from that, I think that's enough
of introduction. Let's go to daherb.
daherb: Thanks, and a little bit about me: I would call myself a computational
linguist, even though my Ph.D. officially just says computer science. And I see
myself in the tradition of this slightly outdated xkcd where people try to use
computers to test linguistic theories. In addition to that, I spent my time in
Sweden in a very well known functional programming group and basically next to a
research group dedicated to type theory. So my interests are both into functional
programming, and I got a little bit spoiled also by type theory. And that inspired me
to give this talk. And to start: The question is what is meaning in natural
language? So I came up with a few examples, example sentences. And the
question is: what is the meaning of these sentences? But before we dive into that, a
little bit about linguistics. So there are several subdisciplines in linguistics: one
is syntax, which is mostly people drawing trees. And people are really good at
drawing trees these days. On the slide, you can see various formalisms, how people
draw trees, and that's pretty well established these days. But that's
basically: what are valid sentences in a language? The next question is: what is
the meaning of these sentences? And within linguistics, for a long time, semantics
was something you would not really try to approach because it's really, really
difficult. But actually, semantics is the literal meaning, and in addition to
semantics, we might have the meaning in context. So this is a very great example
of so-called pragmatics. Question: your greatest weakness? Answer of the person:
interpreting semantics of a question, but ignoring the pragmatics. Could you give an
example? Yes. So in this example, the person only looked at the literal meaning.
Can you give an example? Yes, I can give an example. Not interpreted as the request
to actually give an example. So we have the literal meaning and decide that we
even have an additional meaning in context. So if we look at statements in
natural language, we might have challenges in interpreting: what do they mean?
All men are mortal. Every man is mortal.
That we can interpret pretty literal. Yesterday it was raining.
Tomorrow it will be raining. The first one could be a literal fact. The one about the
future. Who knows? Then there are statements about things that could
potentially happen. It could be raining. Then there are statements which in our
world could never actually happen, like John is searching for a unicorn. It's
pretty much a matter of fact that there are no real life unicorns. So if John is
searching for a unicorn, we don't really claim that there might be unicorns in our
world. And then we have questions like, could you pass me the salt where we don't
really have the literal meaning or we don't care about the literal meaning, we
don't care if the answer is yes or no. What we actually – what the person
making the statement actually means is, please hand me the salt. Please pass me
the salt. And in addition, there is kind of an assumption that there is actually
salt on the table. But we don't really assume that if John is searching for a
unicorn, that there is a unicorn, if someone asks the question, can you pass me
the salt? there is actually salt on the table. So meaning is a very philosophical
problem. And why do people care about it? There are relevant questions, for example,
when are two statements equivalent, when do they mean the same? "All men are
mortal" Does it mean the same as every man is mortal? Or the more challenging "I saw
the morning star", "I saw the evening star" "I saw Venus". As a matter of fact,
these three are meaning exactly the same, but if someone says, I saw the morning
star, do we know that they actually also know that they saw Venus, that the morning
star is the same as Venus? And another relevant question is, when does one
statement follow from other statements? And especially in computational
linguistics, we want to find automatic ways to decide these questions. There are
a few more examples. So there is a very well-known example: all men are mortal,
Socrates is a man. So we should come to the conclusion that Socrates is also
mortal. Or more challenging: every European, has the right to live in Europe.
Every European is a person. Every person who has the right to live in Europe can
travel freely in Europe. Can we answer the question, can every European travel
freely within Europe? and hopefully find some way to answer this question with yes.
Humans are – People are usually pretty good at deciding that with a little bit of
logic and a lot of intuition. But computers are really bad about intuition.
So we are interested in models or ways that actually also work for computers. And
these days there are basically two big branches: the one the formal approaches.
And the other are the statistical approaches. The formal approaches use
logic to try to answer the questions, while the statistical approaches, just
look at plenty of data, I shouldn't say "just", they use a lot of data to answer
the questions we are interested in. In this talk, I will only focus on the
formal approaches because I like them more. But both approaches, both kinds of
approaches have the right to exist and can be also very helpful in their own way. So,
back to the kind of the title of the talk now slightly paraphrased: type theory and
semantics. And there are basically two big approaches to type theory. OK, what is
type theory? In computer science type theory is the study of what systems of
types exist and how, what properties do they have? We will shortly see what
that could mean. So that … If we go back in history, then there are simply typed
languages. They go back to Alonzo Church. I think in 1940 he described the
simply typed lambda calculus. And then a few decades later, a guy called Richard
Montague used this approach or adopted this approach, which was purely from logic
to natural languages. And Richard Montague was a very particular person. He was … he
had a great influence, but also he was not an easy person, he openly attacked
colleagues and … but his influence on linguistics started in the 70s. There are
still people trying to work out details about his theory. Now we come to the
one answer: what is meaning in linguistics? And that's so-called truth
conditional or model theoretic semantics. So, what is the meaning of the sentences
like "all men are mortal". And the meaning of this sentence is: can we come up with a
model which is kind of a picture of a world that makes this sentence true? And
here in the picture, we have an example of that: we have the set of all mortal
things. And we have the set of all men in our world, and they are a subset, meaning
everything that's a man is also a mortal thing. And then we have the second
sentence, which says "Socrates is a man", which means we know that Socrates is one
of these objects in the set of all men. And then is the question "is Socrates
mortal?", and because we know that all men are in the set of mortal things, we can
answer this question quite easily with yes. So one approach to meaning of natural
language is: can we find a world in which all the properties are in a way that all
the sentences we are given are true? And because we look at models, it's called
model theoretic semantics. And the big influence of Montague was … As I mentioned
before, there was already the theory by Alonzo Church of the simply typed lambda
calculus, which was an approach in logic, and then there came around Montague and
made the statement, this very bold statement: "There is, in my opinion, no
important theoretical difference between natural languages and the artificial
languages of logicians. Indeed, I consider it possible to comprehend the syntax and
semantics of both kinds of languages that think a single natural and mathematically
precise theory". And that's a really bold statement, because we know that usually if
we, for example, look at programming languages, they are very small and very
well-defined compared to what we can express in natural languages. But yeah, he
made the statement and then he started to demonstrate that this is actually
possible. Then, let's look a bit at times, and I called this a simply typed language,
and we can give … We have infinitely many types, and every object in our
logic language has a type. And the type is either e for an
entity, t for truth value, or if we have some type alpha, and some other type beta,
then we have this pair , which is a type. And then logicians like to be
very precise and they say "nothing else is the type in this language". And. That's,
again, rather abstract. Let's look at some examples. We have certain classes of words
in our language. For example, we have names. And they … our examples are, for
example, John and Mary, and we have the semantic type e, which is a basic type,
and then we have intransitive verbs, which means verbs that don't take a direct
object like "sleeps" or transitive groups that have a direct object like "love". And
then we have sentences and they have the semantic type t, which is as a computer
scientist, I would call it boolean. It's a truth value. It's either true or false.
And intransitive verbs have this type of a pair ("e to t"), which, for example,
could interpret as a function from entities to truth values. And then I have a
few examples down here. So what's in this double square brackets? That's our natural
language. And what's not in italics, not in these double square brackets, that's our
logic language. So for simple things like the name John, we just claim that there's
some object representing John, we call it just "j". The same for Mary and also "sleeps"
and "love", we translate to just some object in our logic language. But what are
these exactly? There are two ways to look at them: sleep' ("sleep prime"), for example,
is either the set of all objects that are sleeping in our world. For example, the
set only consisting of only having the element John or j representing John. So
John is the only sleeping entity in our world, or we can represent it as a
function from entities to truth values and the function returns true, if x is a
sleeping element in our world and false otherwise, and if we define it the
following way, that j is mapped to true and m is mapped to false, then we get
exactly the same representation as with the set before. And that theory, that's
usually called a characteristic function. So either we can treat it as a set or as a
function. In this case, it doesn't really matter, but the next question is: "what is
love?" Or love', to be precise. And while "sleep" is a property of an entity –
for each entity, we can decide if it's sleeping or not. Love is not a property of
one entity, but it's the relation between two entities. So it's either a set of
pairs. Or it is a function which takes two parameters, and as soon as we apply to one
of the parameters, we end up with the second function. So the function with two
parameters represent the relation between two entities or two individuals. But if we
apply to one of the parameters, we get a function, which is the property, for
example, to be loved by someone. Just to keep in mind, for simple predicates, sets
and functions are equivalent, and for these relations, it's either pairs or it's
a function. And if we apply it to one of the arguments, we get another function.
One of the driving forces behind the theory of Montague is compositionality.
And that's usually attributed to Frege, even though he never really expressed it
that way. But one of the most well known interpretations is "the meaning of a
compound expression is a function of the meaning of its parts and the way they are
syntactically combined". So if we go back here, we kind of have our simple and
simplest parts. We have our names and we have our verbs, and we have rather simple
interpretations what they mean. And now the question is how can we combine them to
form … for example, the meaning of more complex sentences, or in general of
sentences. And for that, we need a little bit of syntax. Syntax tells us how we can
combine these elements to form sentences. So the rule syntax 1, for example, says if
we have a name and an intransitive verb, we can combine them to a sentence. And the
second rule, syntax 2, says if you have a transitive verb and a name, we can combine
it to an intransitive verb. Now we want to look at the meaning of sentences like
"John sleeps" and the meaning of "John sleeps" is that if we interpret the
meaning of "sleeps" and that's the predicate which can be applied to an
entity or an individual to give a truth value. And John is of type e, so we can apply
sleeps to John and we get, as a result, sleep' applied to John. Or the
slightly more complex example of "John loves Mary". We can first apply the same
semantic rule that we can apply the rest of the sentence to the subject of the
sentence. And then we have to interpret "loves Mary", which is this function that
takes two parameters and then is first applied to the object and then to the
subject. So the meaning of "loves Mary" is kind of the predicate "to be in in a state
of loving Mary". And then we apply to John and we get the meaning: Love, Mary, John.
And now the question is: how do we actually come up with these semantic
rules? So how do we know that we have to apply "loves Mary" to "John". And that's
where the types give us guidance. So we know that "loves Mary" is of the Category
IV, intransitive verb, which has the type , and we know that John is of the
category "m", which is of semantic type e, and if we see as a function which
takes an "e" as a parameter to produce a "t" as a result, then we know that we can
apply "loves Mary" to John. Then I already before mentioned the word lambda calculus
or lambda expression: Probably not everyone knows what a lambda
expression is. It's kind of the solution to a very … almost nit picky problem. So
if we have some formula, some expression like "x^2 + 2 x", what does it
exactly mean? And then we could come up with just putting numbers instead of x.
And if we put 1, we get the result 3 and if we put 2 the result is 8 and if we put
x=3, we get 15. But what we usually mean is: it's some kind of function
which takes a number and then maps this number to the number's square plus two x.
That's what we mean. But it's not really written down precisely. And that's where
logicians came up with a new operator called lambda. Which can introduce a
variable and turn up expression, which is not completely clear, like the one we had
before into a function. So if you write "lambda x, x^2 + 2 x", we know
that it is a function which has a parameter which we call x, and we use that
in our expression "x^2 + 2 x". And then we can apply this, for example,
to 1, which means we have to replace all "x"s in our expression by 1, and then we
get exactly the same results as we had in our informal expression. But now it's on a
proper foundation. Why do we need that? Because we actually have, kind of higher
order types, so we know that the E to T is kind of a function from individuals to
truth values, that that's the same for common noun like man, bird and so on. But
what is the type of what we call determiners or quantifiers: some, every,
the. So the meaning of man is just man' or man'(x), the same
as we have had with sleep before. And the meaning of "every" now we
use this lambda. Because the meaning of "everything" is for all things "x" that are
individuals, if they meet some predicate P, then they also meet some predicate Q.
That's, again, very abstract, so let's have a look at an example. So the meaning
of "every man" is: We have a new semantics rule meeting all the types, so the type of man
is and the semantic type of "every" is this a slightly more complex type, but
is the function from to something else? So we know we can apply that terminal
to our common noun. Then we do our lamda magic and we end up with the term lamda Q
for all x, man'(x) implies Q(x), meaning for all things: If they are men, then they do
something or they have a certain property. And if we now look at "every man sleeps".
We apply "every man" to "sleeps", we just had this term on the previous slide and the
types for Q and for sleeps match, so we can just put that in there. And the
meaning of "every man sleeps" is for all individuals: If they are men, then they
sleep. And that way we get a theory how we can translate expressions of natural
language into expressions, into logic expression, for which we can try to find
models, so we have this truth conditional semantics, and it is compositional in the
way that the meaning of an complex expression depends on its components. The
meaning of "every man sleeps" depends on the meaning of "every man" and of "sleeps"
and on ways how to combine them. And these ways how to combine them are determined by
the types we use. So we have some very nice method of computing meaning in a
compositional way into a logic, so that looks already pretty much like what
Montague claims, but it has certain drawbacks. And for that reason, and also
because in logic and computers science the research progressed, people came up with
the so-called MTTs "Modern type theories" or the original is called "Martin-Löf type
theory". So this nice bearded guy on the left is kind of the person who invented
everything and the nice person on the right who likes to climb mountains, he
used to be … who is a professor in the group where I was doing my Ph.D. used
these type theories, these modern type theories to express the meaning of natural
language in a slightly different way. And I'll give a quick glance at what changes
they have. But first, one of the big advantages of this – or one of the biggest
implications of these modern type theories is usually in computer science, in proof
systems. So one of the most or very well- known proof assistant is the one with the
logo on the right called Coq. Another dependently type programming language is
the language Agda, which is … both of them are used quite extensively in formalizing,
and verifying, for example, proofs in mathematics, and verifying and proving
properties about programs. But they can also be used to reason about natural
language. So the different approach to meaning in language is the so-called proof
theoretic semantics. So before we looked at what models can be, how models can be
used to express conditions under which things can be can be seen as true. And now
we care more about proofs than about truth. And that goes back to logic and
computer science again. Where it's usually referred to as the Curry-Howard
isomorphism. It's that proofs in mathematics can be expressed as programs
in a computational framework, and that allows us practical reasoning on
computers. And informally, if you want to prove something, A, we can construct a
term or write a program t of this type. And an example is at the top of the slide
where we kind of want – first it's a function and it's the function from a
semantic representation of the sentence "every man walks" to the sentence "John is
a man", and finally the sentence "John walks". So we want to we have the two
sentences "every man walks" and "John is a man". And we want to get to the conclusion
– or to figure out – if it is a conclusion that "John walks". And this is a small
proof in the proof assistant Coq there in a few lines of code. In a few lines of Coq
code we can find the proof that actually from the sentence every man walks and John
is a man. We can conclude that "John walks". The first big extension is: we
have more expressive types. So before we had the type e for entities and the type t
for truth values. So actually the type t doesn't change a lot. We now just called
it "prop" the type of propositions. But for common nouns like man, which were
properties properties of individuals we just introduced new types
like "man", "book" and so on. And for verbs, for example, we define them as
functions from one of these types to properties. So not just from any
individual, but from meaningful domains. So, for example, the meaning of talk
requires that whoever is talking is actually human, because except for a few
situations where other things could talk, it's usually only a human who talks. And
the meaning of mortal is that something has to first be alive to be mortal. That's
already nice, so we can limit our domains of predicates to very meaningful things
where people intuitively would say that makes sense, but then we end up in the
problem. For example, if we have the meaning of "Socrates is of type man" and
wave "mortal", but mortal is of this type: it takes a parameter that's animate and
return a property. And now we want to interpret "Socrates is mortal" in pretty
much the same way as we did it before, or in a similar way as we interpreted things
before. So we want to apply this meaning of "mortal" to Socrates, but we have the
problem, that man doesn't match the type animate. So how does that work? And the
answer to that, to that is we can assume subtypes, or we can introduce subtypes. So
if we assume that humans are animate and men are human. Then we can actually apply
the function that takes an animate object as a parameter to something that's a man,
and also we want to assume that modified objects like a heavy book should still be
a subtype of book. And fortunately, we can do that in the theory. And the final thing
is: some functions, so we can already rule out some some things, with the … here, if
we say that "talk" only works for humans, we can already rule out some nonsensical
things, but we can use a little bit of this proof theoretic a bit more. So if we
have this. I hope it's not too distracting that it's a bit of a weird
syntax. We define a new type which is consumable, and we define two objects that
are consumable. It's bread and wine. And then we define a new type of action with
the two actions. One is eat, one is drink. And then we define a new type performance,
which depends on both a consumable object and an action. And then we can construct
objects of this performance, by using this construct to perform. So the meaning of
"drink wine", for example, could be: perform, wine, drink. But we can also in
this setting define the meaning of "eat wine" as: perform, wine, eat. And that's
usually something we want to rule out. We want to have only to be able to drink wine
or to eat bread, but not to eat wine or drink bread. And that we can do by
defining a new type of, for example, edible and drinkable objects, and we
define eat bread as edible bread and drink wine as drinkable wine, and then we modify
our action and performance, that the action of eating needs an object of this
type edible for the thing we want to consume. And this object is kind of the
proof that whatever consumable we want to eat is actually edible. And then we can
still define drink wine. In a pretty similar way, but we cannot find any way of
performing eat on wine because there is no way of constructing an edible object for
wine. Which is a very powerful thing of modeling how our real world happens to
work, and … that pretty much concludes my talk. Here are a few references.
And now I'm open for questions. Herald: Right, so, so far we have one
question I see. And the question is: so how far can we take this? Has anyone ever
formulated a sufficiently detailed type system for English or at least some
variant of English, which can be used to reason about human-written or even
informal texts like algorithmic language processing?
daherb: That's a very good question. And that's one of the weak spots of this,
that it involves lots of work. And these days a lot of research and effort is more
on statistical models where you hopefully, very hope, that the computer might learn
these things. There are a few there, there's for example a dataset. So some
logicians sat down at some point and made many sentences in this style, like "every
European has the right to live in Europe" and so on. I think it's a few hundred
sentences and that's kind of the benchmark where people try to test the systems . And
that kind of works. I know there are systems that can cover the whole benchmark
and give the right results, but there are other datasets that are not created by
logicians, but by everyday people crowdsourced on the Internet, and there
it's much more difficult to actually agree on what is the conclusion?
Herald: Okay, so the main problem is that there aren't any curated big enough data
sets to to check the algorithms against, or?
daherb: That's part of the problem. But it's also, yeah, it's really difficult to
make that work for the complete language, for really big parts. But if you have a
small application, a small domain, then it's definitely a feasible thing to do.
And it gives you also an explanation of why one sentence follows from another,
either by giving you the model in which these sentences are true or in the modern
type theory by giving you a proof. So there is lots of research in doing that
without logic and just machine learning, and they seem to be pretty good. But then
sometimes these systems just give you the wrong result and you have no idea why. And
yeah, that's the balance. So you get the highly reliable results from this system,
but you have to do a lot of work to get it working, or you use a machine learning
system which works much broader, but if something goes wrong, it's much more
difficult to figure out what is exactly going wrong.
Herald: Okay, thank you very much. We have a question from Gordon in the IRC –
live.hacc.media for anyone who isn't there yet. How you not managed to mention
Lojban? I'm not really sure on how to pronounce that.
daherb: So, um. I don't know too much about Lojban except that it's an
artificial language that I think was designed to have a clear semantics,
probably something like first order logic so that approach is different and, these
people, at least, who work on this, which I presented at least could pretend that
they work with proper English. Even though some people could also turn it around and
say they defined a nice formal language, which just looks very much like English,
but it's actually it's a formal language. Herald: Okay, and we have Bob asking
whether there is any effort to create a combination of a statistical and logical
approach, and if not, why hasn't it been done or what are the challenges?
daherb: There are definitely approaches that try to do that. The question
is, where do you put the machine learning and where do you put the logic and what
parts you can replace by machine learning, for example? But there is definitely
approaches. I think one is called CCG Lamda by people in Japan.
So there are definitely these approaches. Herald: And we have Klondyke asking
whether there is any work on trying to infer types and rules from the corpuses.
daherb: I'm not really aware of anything like that.
Herald: Did you try generating valid sentences by random.
daherb: depends on what you define as valid sentences. One answer to this
question would be I once wrote a Twitter bot which generates random sentences which
are all total tautologies. So I used many of these techniques I presented to
generate natural language sentences, which all have a certain logic structure.
And if you have a system like that, generating is usually not a big issue,
analysis is usually the bigger issue. Herald: Okay, we have one more question
where I can get the context to about the xkcd cartoon – maybe go back to the slide,
and they want to know whether you can say something about why there are many
competing syntax trees for the same language or more like what the tree is
exactly for, what are the differences daherb: In this, the main difference is
how much effort you want to put into the analysis. So the syntax tree at
the top left is basically textbook level. It gives a very simple analysis and
from a linguistic point of view, people could argue what exactly is, for example,
this category for copula. And the other two sentences are kind of – I don't want
to really say competing syntactic theories, so there are lots of theories,
where they try to explain how natural languages work. I said people are really good at
drawing trees, but they still struggle to explain certain things. And over the last
almost hundred years, people came up with lots and lots of theories, how syntax
actually works. And these theories usually have nice advantages and on the other
hand, drawbacks. So the syntax tree on the top right is called combinatory categorial
grammars and it uses categories which are also kind of function types. So NP/N and
can be seen as a function which takes a N as a parameter on the right and generates an
NP. So the syntactic categories are kind of in parallel to the semantic categories.
And that way it's easy to translate from the syntax tree into the semantic
representation while for other syntax formalisms it might be more challenging to
to do that. So it strongly depends what you want to do, how to express that
concept. Yeah, it goes a bit in the direction of this xkcd. I can subscribe to
any dozen of contradictory models and still be taken seriously.
Herald: Okay, are there any issues on these trees with garden path sentences?
daherb: I should know more about garden path entrances because it's one of
the main examples where things go wrong. At the moment. I cannot really answer
that. I try to give a simple high level overview of it. And there are many
interesting problems: garden path sentences, donkey sentences, where syntax
or semantics or both can go wrong. Herald: Okay, so far, I don't see any more
questions, so I would like to know from you, how does one get into type
theory or language analytics or semantics daherb: Hanging out with the wrong people
or, yeah. So computational linguistics is a pretty established field these days, so
it's what people call interdisciplinary, it's taking a lot of computer science and
hopefully still a bit of linguistics, and then you try to tackle certain problems.
And one of the big problems of natural language is what do they mean? And when
you study that, for example, then you get some you learn something about it, and if
you're curious about it, you can put research into it. And to be honest, my
research was something completely different. But the topic of semantics was
kind of one of the reasons why I wanted to do some more research and stay in
academia. Herald: Okay, thank you. Back again to AI
language processing. Do you think there is a kind of new, bigger field coming? Well,
there was the last few years with natural language processing getting more and more
accessible to the public and better. And do you think that there is still a chance
for only analytical approaches, or do you think that AI will be in the end, more
prevalent? daherb: So actually, if you look at the
research output in recent years, then you only find a little bit about what I was
talking about and you find a lot about … what I have listed here as statistical
approaches, especially language models. I guess most people who haven't been away
from the Internet in the last few months have at least heard a little bit about,
for example, GPT-3, which is one of these fancy AI models which you can use for
generating text based on some sentence to start the text. Or people even
implemented a dungeon crawl text adventure using it. So that's the hot shit in in
research, kind of. But these suffer from this problem that as soon as something
goes wrong, it's really difficult to figure out what's going wrong. And you
need shitloads of data. Herald: Okay, we have some more questions.
Just came in. We have some book recommendations in the IRC if anyone is
interested. And we have one person asking whether a function word like conjunctions
or some grammar like that-clauses can be present in type systems.
daherb: So I haven't done anything about conjunction and so on. In the simply
typed language, they are just translated to their logic operators. So you only have
usually conjunctions on the sentence level so you could make sentences. "John loves
Mary" and "Mary sleeps". And because the type of sentence is t, which is truth
value, which is kind of a boolean variable, you can use boolean operations
on it. So you analyze the first sentence and then you analyze the second sentence
and then you check if the logic conjunction holds between them. And if you
translate that in into models, conjunction can also be translated into the set operation
of intersection. So conjunctions and disjunctions like the
function words "and" and "or" are pretty easy, or still rather easy to express.
There is, …, still many, many challenges which into which I couldn't go in the
time. Herald: Okay. I think that answers the
question from before. And there is also a new one: This "for all" thing. I always
thought that required dependent types. Did I miss something or is that actually
wrong? daherb: If it is a simply typed
language, then it doesn't require dependent types. There is is an equivalent
to the "for all" in dependent types – in dependently typed languages. I think that
should be the Pi types which are dependent function types, but in a simply
typed language you just have the forall operator.
Herald: Okay. Are there new questions? I think there are. Can you recommend an intro
to linguistics or a book? I think we just had some, but maybe, you know, some off
the top of your mind. daherb: So except for the ones I have in
my literature list, there are a few books by a professor called Emily Bender, which
she coauthored with other people. One is about syntax, one is about semantics. And
I haven't read them myself, but I think they are pretty good from what I heard.
Because they also bridge between the linguistic knowledge and the requirements
you have these days with more computational.
Herald: Okay. I think, I'm not sure whether the "no" is directed towards me or
you, but apparently some of these were only programing language books, so
probably the ones in the IRC. There is also a question relayed from Twitter
whether semantic web still is a thing in your community.
daherb: It's a community on its own. And I don't know too much about it. It it's
definitely still a thing. There are still people working on it, but I cannot say too
much about it. I think that was probably going in this direction, new attempts for
multilingual Wikipedia, where you use semantic representation for the Wikipedia
page and then use that to generate the articles in various languages.
Herald: Okay, I think the end – daherb: And of course,
Herald: The IRC, you're already satisfied –
daherb: Maybe another answer to the semantics web and in addition, an answer
to a question that was before about actually inferring these types somehow is
so what you can do with these types, especially with expressive
types, is you kind of create something that's called an ontology, which is in a way
a representation of the world. So what I try to do here is I define what is edible,
what is drinkable, and it's tedious to hard code all these things about the
world. And a lot of this is represented in either datasets or, for example, in the
semantic web. So people already put effort into encoding that somehow and then you
just need to extract it and use it. Herald: Okay, we are already at the end
of time, there is three minutes left. We have one more question. I think after that
we'll close it: And are you aware of natural language, hand-wavy formal text
like codes of law which have been type checked?
daherb: I know that there are people who spend their whole Ph.D. on trying to
formalize law texts. I think there was also
some work on formalizing the GDPR, but I heard about a few of these things, but
I'm not fully aware of what's available and where it is available.
Herald: Okay, so if you don't have anything more to say, say so. And apart from that,
I think we are done here, at least for my part.
daherb: Yep, then thanks for listening!
*postroll music*
Subtitles created by c3subtitles.de in the year 2021. Join, and help us!