New answers tagged type-theory
6
If we keep reducing the right subterm, then yes, we will never get to $v$. But noone says that we are restricted to this decision. The Church-Rosser theorem does not claim that any possible reduction series must lead to $N_3$. Church-Rosser just states that $N_2 \twoheadrightarrow_\beta N_3$, i.e. that there exists some beta reduction series that will lead ...
3
There are potentially multiple ways of presenting canonicity (and I think complications depending on the theory). However, I think the simplest way to think about it is from the perspective of a programmer wanting to use the type theory to compute something. For instance, we might want to compute some natural number satisfying some specification we've come ...
2
What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $a$ and $b$, it normalizes both of them (based on judgemental ...
5
Supposing we have $a$ and $b$ of type $A$ and $p : \mathrm{Id}_A(a,b)$, there simply is not any rule of type theory that would allow you to replace $b$ with $a$ arbitrarily. So one answer is "because type theory does not let you do that", and if you think that it can be done, please show me how. But I suppose that is a non-answer, what you really are asking ...
4
We don't always want extentionality
In mathematics, a function is a relation between its inputs and its output. Two functions are equal if and only if they map the same outputs to the same inputs. But in computer science, we're often interested in descriptions of computations which we also call “functions”, where it matters how the outputs are calculated ...
2
what does it mean by becoming extensional in the first place?
The axiom of extensionality relates to what it means for two functions to be equal. Specifically, extensionality says:
$f = g \iff \forall x \ldotp f(x) = g(x)$
That is, functions are equal if they map equal inputs to equal outputs. By this definition, quicksort and mergesort are equal, even if ...
5
Recall that (a few paragraphs above)
two objects are definitionally equal if after certain computation steps they evaluate
to identical results.
Assume throughout this post that $M$ and $N$ are definitionally equal. This means that there is a series of computation steps $M_0 \leftrightarrow M_1 \leftrightarrow \ldots \leftrightarrow M_n$ where I use $\...
9
A major idea of concatenative languages is that the syntax and semantic domain form monoids and the semantics is a monoid homomorphism. The syntax is the free monoid generated by the basic operations, better known as a list. It's operation is list concatenation, i.e. (++) in Haskell. In the untyped context, the semantic domain is just the monoid of ...
2
There will be no inconsistency. Those arise from shady postulates which state that some subkind is an element of itself, or that "too large" a kind/type is an element of a "too small" one (the most famous example is $\mathrm{Type} : \mathrm{Type}$), but that is not what we are dealing with here.
To give an example of what you're looking for, take $\mathrm{...
Top 50 recent answers are included
