NOTE: Lambda Cube
source link: https://dannypsnl.github.io/blog/2020/09/17/cs/note-lambda-cube/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
First we have UTLC(untyped lambda calculus) to STLC(simply typed lambda calculus), by adding arrow type(): Lambda cube Lambda cube starts…NOTE: Lambda Cube
Email: [email protected]
GitHub: @dannypsnl
Twitter: @dannypsnl
Programming Language Theory • System Programming
NOTE: Lambda Cube
First we have UTLC(untyped lambda calculus) to STLC(simply typed lambda calculus), by adding arrow type(→\to→): λx:Nat.x\lambda x:Nat.xλx:Nat.x
Lambda cube
Lambda cube starts from STLC.
STLC -> λ2\lambda 2λ2
Terms depend on Types: λ(a:∗).λ(x:a).x\lambda (a : *).\lambda (x:a).xλ(a:∗).λ(x:a).x
λ2\lambda 2λ2 -> λω\lambda \omegaλω
Types depend on Types: λ(a:∗).a→a\lambda (a : *).a \to aλ(a:∗).a→a
λ2\lambda 2λ2 -> λΠ\lambda \PiλΠ (Π\PiΠ type)
Types depend on Terms: Π(x:a).M\Pi (x : a).MΠ(x:a).M
COC(calculus of construction)
Mix Π\PiΠ and λ\lambdaλ, type is term.
COC = λ2\lambda 2λ2 + λω\lambda \omegaλω + λΠ\lambda \PiλΠ
CIC(calculus of inductive construction)
Introduce Inductive, e.g. data Nat = zero | suc Nat
CIC = COC + Inductive
author: Lîm Tsú-thuàn/林子篆/Danny
category:cs
tag:notepltlambda cube
Similar Articles
All works in this site is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK