# Tagged Questions

For questions on the formal system in mathematical logic for expressing effective functions, programs and computation, and proofs, using abstract notions of functions and combining them through binding and substitution.

155 views

### Proper full submodels of full models of type theory

Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full ...
77 views

### Understanding Strong Normalization for Identity Types in Martin-Löf Intensional Type Theory [closed]

Roughly, the strong normalization property for Martin-Löf Intensional Type Theory (MITT) tells us that every closed term $t$ of type $M$ will eventually reach a canonical normal form $t’$ such that it ...
196 views

### Easier Girard's paradox in a circular pure type system (PTS)

System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox. One-...
317 views

### Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called reflection rule that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$...
239 views

### Comparing really big numbers

Is there an intractability theorem that says that in any sufficiently rich system for defining really big numbers, there will be two numbers for which it's very, very, ... very difficult to decide ...
70 views

### Optimal reduction using token-passing nets

I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis ...
162 views

### On an automatic translation of typed lambda calculus in untyped lambda calculus

I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus. Take for example the inductive definition of lists, with introduction rules: and: We can ...
216 views

171 views

### Is it possible to implement η-reduction in interaction nets?

There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ...
658 views

### Turing-complete primitive blind automata

Let $N$ be the set of natural numbers, $S$ be the set of finite binary sequences, and $Q = [N \rightarrow N] \times [N \rightarrow N],$ where $[N \rightarrow N]$ is the set of all computable ...
252 views

### Universality of blind graph rewriting

Let us consider $S(M) = \{(f_0, f_1) | f_0, f_1: M \rightarrow M\}$, where $M$ is a finite set. Each element of $S(M)$ is equivalent to a finite directed graph with the set of nodes $M$, which has ...
819 views

### Algebraic structure generated by primitive graph operations

Let $M$ be a finite set, and $S(M) = \{(f_0, f_1) | f_0, f_1: M → M\}$. Each element of $S(M)$ can be considered as a finite directed graph with the set of nodes $M$, which has exactly two arrows ...
370 views

### Difference between lambda-calculus with well-formed formulas vs properly-formed formulas

In S.C. Kleene's 1935 paper "$\lambda$-definability and recursiveness," he proves that all $\lambda$-definable functions are general recursive in the Herbrand-Godel sense and vice-versa. However, the ...
7k views

### What is some good introduction to lambda calculus?

I have some background in set theory and automata and I am looking for a good place to start with lambda calculus.
831 views

### Why is alpha-equivalence in untyped $\lambda$-calculus substitutive?

This is something all introductory texts seem to avoid proving, and many even avoid stating. We consider untyped $\lambda$-terms on some countably infinite alphabet. If $x$ is a variable and $p$ is ...
392 views

1k views

### Scott on the consistency of the lambda calculus

I have twice heard it attributed to Dana Scott that he said something to the effect that the consistency of the lambda-calculus was an accident. Does anyone have a reasonable-sounding source for this?...
1k views

### Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
5k views

### Is functional programming a branch of mathematics?

In Theory mainly concerned with lambda-calculus?, F. G. Dorais wrote, of the idea that the lambda-calulus defines a domain of mathematics: That would never stick unless there's another good reason....
### Theory mainly concerned with $\lambda$-calculus?
Automata theory is mainly concerned with Turing machines and all its relatives-in-spirit. $\lambda$-calculus is rather rarely mentioned in textbooks on automata theory. What's the common name of the ...