Skip to main content
Stack Overflow Jobs powered by Indeed: A job site that puts thousands of tech jobs at your fingertips (U.S. only). Search jobs

Questions tagged [normalization]

The tag has no usage guidance.

6 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6 votes
0 answers

Locally-nameless representation: normal order & opening with a bound variable

This question concerns the representation used in Arthur Charguéraud's paper “The locally nameless representation” and is somehow a follow-up on this question, where it is asked about the ...
phipsgabler's user avatar
3 votes
0 answers

Expansion normal forms of confluent term rewriting systems

Suppose one has two rewrite rules $\to^\eta,\to^\beta$, both of which are confluent and such that $\to^A := \to^{(\eta \cup \beta)}$ is also confluent. Define a $\beta$-normal form relative to $\eta$ ...
Jonathan's user avatar
2 votes
0 answers

Variable opening in locally-nameless representation

Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
phdstudent's user avatar
2 votes
0 answers

MLTT/MiniTT: why do normal forms of sum types carry environments?

I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types. A ...
Siddharth Bhat's user avatar
1 vote
0 answers

Is it possible to define beta reduction for PHOAS?

I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml: ...
Hirrolot's user avatar
  • 105
0 votes
0 answers

Simple Lambda Calculus Question

For any 2 strongly normalizing terms in the simply typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong ...
Abhishek Manikandan's user avatar