Explicit substitution

Inom datavetenskap sägs lambdakalkyler ha explicita substitutioner om de ägnar särskild uppmärksamhet åt formaliseringen av substitutionsprocessen . Detta är i motsats till standard lambda-kalkylen där substitutioner utförs genom beta-reduktioner på ett implicit sätt som inte uttrycks i kalkylen; "friskhets"-förhållandena i sådana implicita kalkyler är en ökända källa till fel. Begreppet har dykt upp i ett stort antal publicerade artiklar inom ganska olika områden, såsom i abstrakta maskiner , predikatlogik och symbolisk beräkning .

Översikt

Ett enkelt exempel på en lambdakalkyl med explicit substitution är "λx", som lägger till en ny form av term till lambdakalkylen, nämligen formen M⟨x:=N⟩, som lyder "M där x kommer att ersättas med N" . (Betydningen av den nya termen är densamma som det vanliga idiomet låt x:=N i M från många programmeringsspråk.) λx kan skrivas med följande omskrivningsregler :

(λx.M) N → M⟨x:=N⟩
x⟨x:=N⟩ → N
x⟨y:=N⟩ → x (x≠y)
(M ₁ M ₂ ) ⟨x:=N⟩ → (M ₁ ⟨x:=N⟩) (M ₂ ⟨x:=N⟩)
(λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y och x inte fria i N)

Även om substitutionen görs explicit, behåller denna formulering fortfarande komplexiteten hos lambdakalkylens "variabelkonvention", vilket kräver godtyckliga byte av variabler under reduktion för att säkerställa att villkoret "(x≠y och x inte fritt i N)" på den sista regeln är alltid nöjd innan regeln tillämpas. Därför undviker många beräkningar av explicit substitution variabelnamn helt och hållet genom att använda en så kallad "namnfri" De Bruijn-indexnotation .

Historia

Explicita ersättningar skisserades i förordet till Currys bok om kombinationslogik och växte fram ur ett "implementeringstrick" som till exempel användes av AUTOMATH , och blev en respektabel syntaktisk teori i lambdakalkyl och omskrivningsteori . Även om det faktiskt har sitt ursprung med de Bruijn , är idén om en specifik kalkyl där substitutioner är en del av objektspråket, och inte av den informella metateorin, traditionellt krediterad till Abadi , Cardelli , Curien och Lévy. Deras uppsats om λσ-kalkylen förklarar att implementeringar av lambda-kalkyl måste vara mycket försiktiga när de hanterar substitutioner. Utan sofistikerade mekanismer för strukturdelning kan substitutioner orsaka en storleksexplosion, och därför försenas i praktiken substitutioner och registreras explicit. Detta gör överensstämmelsen mellan teorin och implementeringen mycket icke-trivial och riktigheten av implementeringar kan vara svår att fastställa. En lösning är att göra substitutionerna till en del av kalkylen, det vill säga att ha en kalkyl av explicita substitutioner.

När substitution har gjorts explicit ändras dock de grundläggande egenskaperna för substitution från att vara semantiska till syntaktiska egenskaper. Ett viktigaste exempel är "substitutionslemma", som med beteckningen λx blir

(M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (där x≠y och x inte är fria i P )

Ett överraskande motexempel, på grund av Melliès, visar att sättet som denna regel är kodad i den ursprungliga kalkylen för explicita substitutioner inte är starkt normaliserande . Efter detta beskrevs en mängd kalkyler som försökte erbjuda den bästa kompromissen mellan syntaktiska egenskaper hos explicita substitutionskalkyler.

Se även