Unique Terms

Published: 2021-09-01

Tags: computics

Abstract

Some terms are uniquely (up to normalization and α-renaming) determined by their types.

§ In the polymorphic λ-calculus (System F)

The polymorphic λ-calculus has the following grammar

<judgment> ::= <term> :: <type>

<type> ::= * | <var> | <type> -> <type>

<term> ::= unit
         | <var>
         | λ <var>* . <term> | <term> <term*>

with the usual typing rules.

The following judgements are uniquely determined by the type (up to normalization and α-renaming):

id = λ x . x :: a -> a

apply = λ f x . f x :: (a -> b) -> a -> b

const = λ x y . x :: a -> b -> a

inj1 = ...
inj2 = ...
case • of { inj1 • -> • | inj • -> • } = ...
proj1 = ...
proj2 = ...
( • , • ) = ...
( • , • , ... ) = ...

proj<i> = proj2 o ... o proj2 o proj1 :: (... * a * ...) -> a

§ In the dependently-typed λ-calculus

<judgment> ::= <term> :: <term>

<term> ::= U
         | Π (<var> : <term>)* . <term>
         | λ <var>* : <term>
         | <term> <term>
         | <var>

The following judgments are uniquely determined (up to normalization and α-renaming).

id = λ A x . x :: Π (A : U) (x : A) . A

apply = λ A B f x . f x :: Π (A : U) (B : U) (f : A -> B) (x : A) -> B

const = λ A B x y . x :: Π (A : U) (B : U) (x : A) (y : B) -> A

§ Signature

The following code block is the Ed25519 signature of this post's markdown content encoded in base 64, using my secret key and public key.

b5699ca022c97a4a51529d34b5d63b285244465f06cf70004e442bfaa77b6ac53987b8b77eed71263e13520b47b41b22809159941b18aa67bb42eea98ec07d04

See Signature for more information.