Matroids Matheplanet Forum Index
Moderiert von matph
Informatik » Programmieren » Grundlegende Fragen zu Lean
Autor
Universität/Hochschule Grundlegende Fragen zu Lean
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Themenstart: 2021-11-20

Hallo allerseits, Um die Grundlagen der Programmiersprache Lean zu verstehen, beschäftige ich mich mit dem folgenden Skript: https://cs.brown.edu/courses/cs1951x/static_files/main.pdf Ich habe dort ein Verständnisproblem für Terme und Typen. S.7 steht dort: Given a type σ (which may be a function type), you can use any constant c or variable \(x : τ_1 → · · · → τ_n → σ \) to build a term of that type. For each argument, you need to put a placeholder, yielding c _ . . . _ or x _ . . . _. Ich verstehe Folgendes nicht bzw. interpretiere es so: Gegeben sei ein beliebiger Typ σ Ist dann eine beliebige Variable x oder eine beliebige Konstante c ein Term mit Typ \(τ_1 \: → \: · · · → \: τ_n \: → \: σ \) ? Oder ist dann (für beliebige \(x, x_1, x_2, ... x_n \) bzw. \(c, c_1, c_2, ... , c_n\)) \(x \: x_1 \: x_2 \: ... \: x_n\) bzw. \(c \: c_1 \: c_2 \: ... \: c_n \) ein Tem vom Typ \(τ_1 \: → \: · · · → \: τ_n \: → \: σ \) mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.1, eingetragen 2021-11-20

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) Weder, noch. Sondern: Wenn $x : τ_1 → · · · → τ_n → σ$, dann ist für beliebige Terme $t_i : \tau_i$ $x\, t_1 \dots t_n$ ein Term von Typ $\sigma$. Im Text werden Platzhalter benutzt für die $t_i$ benutzt.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.2, vom Themenstarter, eingetragen 2021-11-21

\quoteon(2021-11-20 16:08 - tactac in Beitrag No. 1) Weder, noch. Sondern: Wenn $x : τ_1 → · · · → τ_n → σ$, dann ist für beliebige Terme $t_i : \tau_i$ $x\, t_1 \dots t_n$ ein Term von Typ $\sigma$. Im Text werden Platzhalter benutzt für die $t_i$ benutzt. \quoteoff Danke für diese Info. Auf S.7 des Skripts steht: "If the type is of the form σ → τ, a possible inhabitant is an anonymous function, of the form λx, _, where _ is a placeholder for a missing term. Lean will mark _ as an error; if you hover over it in Visual Studio Code, a tooltip will appear, specifying the type of the missing term (here, τ) as well as any variables declared in the local context." Ich habe das leider auch nicht verstanden bzw. so interpretiert: Wenn es einen Term t vom Typ $\sigma → \tau$ gibt, (also $t: \sigma → \tau$), dann gibt es eine Variable x und einen Term $\alpha$ mit $t = \lambda x.\alpha$ und zusätzlich - so meine Interpreation - muß $\alpha$ den Typ $\tau$ haben. Ist meine Behauptung korrekt ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.3, eingetragen 2021-11-21

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) Wenn das verwendete = syntaktische Gleichheit bedeuten soll, ist die Behauptung falsch. Wenn es eher semantische Gleichheit sein soll, ist sie wahr (man nehme $tx$ als $\alpha$). Aber im Text steht etwas ganz anderes: Ein möglicher Bewohner von Typ $\sigma \to \tau$ ist ein Term der Form $\lambda x:\sigma. \alpha$, mit $\alpha$ ein Term vom Typ $\tau$.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.4, vom Themenstarter, eingetragen 2021-11-21

Hallo tactac, Erts mal herzlichen Dank für dein Feedback. Habe die Ausssagen auf S.7 (step1 und step2, abgekürzt S1 und S2) für mich (nach deinen Antworten) wie folgt interpretiert: S1) Ein möglicher Term mit Typ $\sigma \to \tau$ ist ein Term der Form $\lambda x:\sigma. \alpha:\tau$ (also: $\alpha$ ist ein Term mit Typ $\tau$ ist). S2) Wenn x den Typ $\tau_1 \to \tau_2 \to · · ·\to \tau_n \: \to \: \sigma$ hat, also $x:\tau_1 \to \tau_2 \to · · ·\to \tau_n \: \to \: \sigma$, dann gilt für beliebige Terme $t_i:\tau_i$ Folgendes: $x t_1 \: t_2 \: · · ·\: t_n$ ist ein Term mit Typ $\sigma$, also: $x t_1 \: t_2 \: · · ·\: t_n:\sigma$ Ist das so korrekt? Wenn das so korrekt ist, werde ich damit das Beispiel auf S.8 bearbeiten. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.5, eingetragen 2021-11-21

\quoteon(2021-11-21 18:44 - carlox in Beitrag No. 4) Ist das so korrekt? \quoteoff Ja.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.6, vom Themenstarter, eingetragen 2021-11-22

\quoteon(2021-11-21 20:52 - tactac in Beitrag No. 5) \quoteon(2021-11-21 18:44 - carlox in Beitrag No. 4) Ist das so korrekt? \quoteoff Ja. \quoteoff Danke für deine Antwort. Ich habe noch 2 Probleme: 1) Was ist ein möglicher Term? Wie formalisert man das Wort möglich in: S1) Ein möglicher Term mit Typ $\sigma \to \tau$ ist ein Term der Form $\lambda x:\sigma. \alpha:\tau$ (also: $\alpha$ ist ein Term mit Typ $\tau$ ist). 2) Ich suche einen Term der folgenden Typ hat: $\alpha \to \alpha$ Wie kann man da argumentieren, wenn man nur von "möglichen" Termen ausgehen kann? Ich brauche irgendetwas Initiales, so wie ein Axiom, also einen Term von dem man sagen kann, dass er von dem oder dem Typ ist. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.7, eingetragen 2021-11-22

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) 1) Du kannst das "möglich" auch einfach weglassen. Im Zusammenhang mit der Suche nach einem Term mit einem bestimmten Typ, kann man die Partikel aber vielleicht so verstehen, dass es vielleicht zum Ziel führt, einen Term von Typ $\sigma$ zu finden, wenn man versucht, Terme $t: \tau \to \sigma$ und $u: \tau$ zu finden (und die dann eben zu einer Applikation zusammensetzt). 2) Irgendein $\lambda x: \alpha. t$ mit $t:\alpha$ geht, wobei in $t$ die Variable $x$ (die den Typ $\alpha$ hat) vorkommen darf. Im Fall von Funktionstypen geben Einführungs- und Eliminationsregeln Terme an $$\begin{array}{c} \Gamma, x: \tau \vdash M: \sigma \\\hline \Gamma \vdash (\lambda x: \tau. M): \tau \to \sigma \end{array}(\to\text{intro}) \qquad \begin{array}{c} \Gamma \vdash M: \tau \to \sigma\qquad \Gamma \vdash N: \tau \\\hline \Gamma \vdash M N \colon \sigma \end{array}(\to\text{elim}) $$ Variablen sind natürlich auch Terme: $$\begin{array}{c}\hline\Gamma,x:\tau \vdash x:\tau \end{array}$$\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.8, vom Themenstarter, eingetragen 2021-11-23

Hallo tactac, I) \quoteon(2021-11-22 14:50 - tactac in Beitrag No. 7) 2) Irgendein $\lambda x: \alpha. t$ mit $t:\alpha$ geht, wobei in $t$ die Variable $x$ (die den Typ $\alpha$ hat) vorkommen darf. \quoteoff Die Aussage von dir müsste man mit den Regeln unten beweisen, oder ? II) Zitat S.6 des o.g. Skripts: (Definition lokaler Kontext) ============================ "A typing judgment has the form C |- t : σ, meaning that term t has type σ in local context C. The local context gives the types of the variables in t that are not bound by any λ. The local context is used to keep track of the variables bound by λ’s outside t." ============================ Meine Interpretation: Der lokale Kontext ist die Menge der Typen derjenigen Variablen in t, die nicht durch ein $\lambda$ gebunden sind, also frei vorkommen. Ist das richtig? III) Etwas weiter unten im Text werden die folgenden 4 Regeln angegeben: Regel1: ----------- Cst if c is declared with type σ C |- c : σ Regel2: ------------ Var if x : σ is the last occurrence of x in C C |- x : σ Regel3: C |- t : σ → τ C |- u : σ ----------------------------- App C |- t u : τ Regel4: C, x : σ |- t : τ -------------------------- Lam C |- (λx : σ, t) : σ → τ Sind das die gleichen, die du im letzten Beitrag vorgestellt hast? IV) a) Hier die 1. Regel: ----------- Cst if c is declared with type σ C |- c : σ C ist der lokale Kontext, also die leere Menge, denn c ist ein "Atom", also kommt in c keine Variable vor, also erst recht nicht eine freie Variable. Warum lässt man das C dann nicht einfach weg vor dem |- ? b) Hier die 2. Regel: ------------ Var if x : σ is the last occurrence of x in C C |- x : σ C ist der lokale Kontext, also die Menge, die nur aus dem Element x besteht, denn in x kommt kein $\lambda$ vor, also kann x auch nicht durch ein $\lambda$ gebunden werden. Warum schreibt man dann nicht: ------------ Var if x : σ is the last occurrence of x in C {x} |- x : σ Und welchen Sinn soll der Zusatz: "if x : σ is the last occurrence of x in C" haben? Der ist doch unnötig, oder ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.9, eingetragen 2021-11-23

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) I) Könnte man. Das wäre jedenfalls ein relativ konstruktiver Beweis meiner Aussage. II) Naja, nicht ganz. Variablen können ja auch durch Quantoren gebunden werden. Außerdem sehen Referenzen auf globalere Konstanten im Term genauso aus wie freie Variablen. Der lokale Kontext listet eben ein paar Variablen auf und weist ihnen einen Typ zu. (Es ist auch keine Menge; die Reihenfolge ist wichtig, da die Typen von Variablen, die "weiter hinten" deklariert sind, auf "weiter vorn" deklarierte Variablen verweisen kann; Wie etwa in $(T, U : \mathrm{Type})(f, g : T \to U)(h : f = g)$ ) III) Im Prinzip ja, wobei ich aber nicht von 'nem lokalen Kontext spreche. IV) a) Zum Beispiel, um zu betonen, dass die Regel für jeden lokalen Kontext funktioniert, und nicht nur für den leeren. b) Ja, das ist recht unschön. Deshalb habe ich eine entsprechende Regel in #7 auch anders hingeschrieben, nämlich ungefähr so, wie du vorschlägst, nur noch mit einem $\Gamma$ als Platzhalter für beliebige weitere Variablendeklarationen.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.10, vom Themenstarter, eingetragen 2021-11-24

\quoteon(2021-11-23 21:33 - tactac in Beitrag No. 9) II) Naja, nicht ganz. Variablen können ja auch durch Quantoren gebunden werden. Außerdem sehen Referenzen auf globalere Konstanten im Term genauso aus wie freie Variablen. \quoteoff Was sind Referenzen auf globale Konstanten im Term? Kannst du mir da ein paar Beispiele und die Definition geben ? (Diese Definition fehlt in dem von mir zitierten Skript). \quoteon Der lokale Kontext listet eben ein paar Variablen auf und weist ihnen einen Typ zu. \quoteoff Wie ist dann der lokale Kontext definiert (ist er eindeutig oder gibt es mehrer mögliche lokale Kontexte)? Kannst du mir dazu ein paar Beispiele geben? Warum wird der lokale Kontext nicht richtig in dem von mir zitiertem Skript definiert? Kannst du mir eine Quelle nennen, wo das richtig definiert wird (mit Beispielen)? \quoteon (Es ist auch keine Menge; die Reihenfolge ist wichtig, da die Typen von Variablen, die "weiter hinten" deklariert sind, auf "weiter vorn" deklarierte Variablen verweisen kann; \quoteoff Also ist der lokale Kontext eine spezielle Liste? \quoteon> Wie etwa in $(T, U : \mathrm{Type})(f, g : T \to U)(h : f = g)$ ) \quoteoff In dem von mir genannten Skript kommen auf S.4 die Allquantoren noch nicht vor. Aber egal. Müsste der von dir genannte Term syntaktisch nicht so geschrieben werden: $(T: \mathrm{Type} \quad U : \mathrm{Type}) \quad (f:T \to U \quad g:T \to U) \: (h : f = g)$ ) wobei $(T: \mathrm{Type} \quad U : \mathrm{Type})$ eine Anwendung ist, $(f:\to U \quad g:T \to U)$ eine Anwendung ist und $(h : f = g)$ syntaktisch sinnlos ist, da nach h: ein Typ stehen müsste. Nach der Definition von Termen und Typen im Skript (S.4 und S.5) wäre der Term von dir syntaktisch nicht zulässig. Wie wird dann der Begriff Term richtig definiert? Kannst du mir eine Quelle nennen, wo das richtig definiert wird (mit Beispielen)? \quoteon III) Im Prinzip ja, wobei ich aber nicht von 'nem lokalen Kontext spreche. \quoteoff Von was dann ? Wie unterscheiden sich deine Begrifflichkeiten von denen in dem von mir genannten Skript? \quoteon IV) a) Zum Beispiel, um zu betonen, dass die Regel für jeden lokalen Kontext funktioniert, und nicht nur für den leeren. \quoteoff Ich habe mich auf die Definition "lokaler Kontext" des Skripts bezogen. Und nach dieser müsste der leer sein, denn c ist ein "Atom", also kommt in c keine Variable vor, also erst recht nicht eine freie Variable. \quoteoff mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.11, eingetragen 2021-11-24

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-11-24 11:46 - carlox in Beitrag No. 10) \quoteon(2021-11-23 21:33 - tactac in Beitrag No. 9) II) Naja, nicht ganz. Variablen können ja auch durch Quantoren gebunden werden. Außerdem sehen Referenzen auf globalere Konstanten im Term genauso aus wie freie Variablen. \quoteoff Was sind Referenzen auf globale Konstanten im Term? Kannst du mir da ein paar Beispiele und die Definition geben ? (Diese Definition fehlt in dem von mir zitierten Skript). \quoteoff Ich meine damit Bezeichner, die weder gebunden sind, noch in dem vorkommen, was da als "lokaler Kontext" bezeichnet wird. So kann man zwar seine Variablen nat nennen, aber das ist kein guter Stil. Und wenn man das nicht tut, ist mit nat eben der vordefinierte Typ der natürlichen Zahlen gemeint. Ein komischer Mix geht auch: \sourceon Lean def silly: nat → nat := λ nat : nat, nat + 5 -- +++ ^^^ --- \sourceoff Der Bezeichner mit --- darunter verweist auf die bei +++ gebundene Variable, der mit ^^^ darunter (und die beiden ganz links in der Definition) meint das globalere nat. \quoteon \quoteon Der lokale Kontext listet eben ein paar Variablen auf und weist ihnen einen Typ zu. \quoteoff Wie ist dann der lokale Kontext definiert (ist er eindeutig oder gibt es mehrer mögliche lokale Kontexte)? Kannst du mir dazu ein paar Beispiele geben? Warum wird der lokale Kontext nicht richtig in dem von mir zitiertem Skript definiert? Kannst du mir eine Quelle nennen, wo das richtig definiert wird (mit Beispielen)? \quoteoff Ich würde sagen, das Skript meint einfach das, was man etwa in VS-Code oder in den online-Varianten im "Info-View" sieht, wenn sich der Textcursor an einer geeigneten Stelle befindet. Eine Quelle habe ich nicht. Es ist auch weniger wirklich etwas logisches oder typtheoretisches, sondern eher etwas, das zum UI-Design gehört. Man will einfach nicht immer alle gebundenen Bezeichner sehen. \quoteon \quoteon (Es ist auch keine Menge; die Reihenfolge ist wichtig, da die Typen von Variablen, die "weiter hinten" deklariert sind, auf "weiter vorn" deklarierte Variablen verweisen kann; \quoteoff Also ist der lokale Kontext eine spezielle Liste? \quoteon> Wie etwa in $(T, U : \mathrm{Type})(f, g : T \to U)(h : f = g)$ ) \quoteoff In dem von mir genannten Skript kommen auf S.4 die Allquantoren noch nicht vor. Aber egal. Müsste der von dir genannte Term syntaktisch nicht so geschrieben werden: $(T: \mathrm{Type} \quad U : \mathrm{Type}) \quad (f:T \to U \quad g:T \to U) \: (h : f = g)$ ) wobei $(T: \mathrm{Type} \quad U : \mathrm{Type})$ eine Anwendung ist, $(f:\to U \quad g:T \to U)$ eine Anwendung ist und $(h : f = g)$ syntaktisch sinnlos ist, da nach h: ein Typ stehen müsste. Nach der Definition von Termen und Typen im Skript (S.4 und S.5) wäre der Term von dir syntaktisch nicht zulässig. Wie wird dann der Begriff Term richtig definiert? Kannst du mir eine Quelle nennen, wo das richtig definiert wird (mit Beispielen)? \quoteoff Ich habe einen Kontext angegeben, keinen Term; und ja, ich habe dabei nicht die Lean-Syntax für Parameterlisten in Definitionen benutzt. Damit hätte ich statt der Kommata Spaces nehmen müssen, um mehreren Variablen den gleichen Typ zu geben. ((T : Type U : Type) geht aber nicht anstelle von T U : Type. ) f = g ist ein Typ. Im Anhang vom HoTT-Buch sollte etwas halbwegs brauchbares stehen für den Anfang (Univalenzkram ignorieren und konkrete Lean-3-Syntax substituieren.) \quoteon III) Im Prinzip ja, wobei ich aber nicht von 'nem lokalen Kontext spreche. \quoteoff Von was dann ? Wie unterscheiden sich deine Begrifflichkeiten von denen in dem von mir genannten Skript? \quoteoff Ich spreche in den Regeln einfach von irgendeinem Kontext. Und im Skript wird sozusagen der eigentlich ziemlich große Kontext in zwei Teile geteilt: den "lokalen Kontext" und den Rest (wobei die Dinge im Rest dort wohl manchmal "Konstanten" statt "Variablen" genannt werden). \quoteon IV) a) Zum Beispiel, um zu betonen, dass die Regel für jeden lokalen Kontext funktioniert, und nicht nur für den leeren. \quoteoff Ich habe mich auf die Definition "lokaler Kontext" des Skripts bezogen. Und nach dieser müsste der leer sein, denn c ist ein "Atom", also kommt in c keine Variable vor, also erst recht nicht eine freie Variable. \quoteoff Man kann auch Terme ohne freie Variablen in einem nicht-leeren Kontext haben. \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.12, vom Themenstarter, eingetragen 2021-11-25

\quoteon(2021-11-24 22:36 - tactac in Beitrag No. 11) Ich würde sagen, das Skript meint einfach das, was man etwa in VS-Code oder in den online-Varianten im "Info-View" sieht, wenn sich der Textcursor an einer geeigneten Stelle befindet. Eine Quelle habe ich nicht. Es ist auch weniger wirklich etwas logisches oder typtheoretisches, sondern eher etwas, das zum UI-Design gehört. Man will einfach nicht immer alle gebundenen Bezeichner sehen. \quoteoff Hallo tactac, Habe keinen VS-Code und Info-View. Leider kann ich mir mittlerweile immer weniger unter einem lokalen Kontext vorstellen. nebel beginnt sich in meinem Gehirn zu verbreiten. Deswegen werde ich mal konkret: x sei eine Variable, c eine Konstante Welchen lokalen Kontext haben folgende Terme: 1) $x \: : \: \sigma$ 2) $c \: : \: \tau$ 3) a) $t \: : \: \sigma \to \tau$ b) $u \: : \: \sigma$ c) die Applikation t u 4) siehe dazu S.6 im Skript: abs $\: : \: \mathbb{Z} \to \mathbb{N}$ 5) siehe dazu S.6 im Skript: x: $\mathbb{Z}$ mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.13, eingetragen 2021-11-26

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) Es ist nicht so, dass Termen Kontexte zugeordnet werden, sondern der Kontext (jetzt mal ohne Aufteilung in lokal/nicht lokal) bestimmt, welche Variablen vorhanden sind, und welche Typen sie haben, und demzufolge, welche Terme überhaupt erlaubt sind, und mitunter, welche Typen diese haben. Im Kontext mit den einzigen Variablen $x : \IN$, $f : \IN \to \IN$ ist * $x$ ein Term vom Typ $\IN$, * $\lambda g\ (z:\IN). g (g\ z)$ ein Term vom Typ $(\IN \to \IN) \to \IN \to \IN$, * $f x$ ein Term vom Typ $\IN$, * $f$ ein Term von Typ $\IN \to \IN$, ... Im leeren Kontext ist $x$ überhaupt kein Term, $f$ auch nicht. Es ergibt keinen großen Sinn, zu fragen, welchen Kontext ein Term hat.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.14, vom Themenstarter, eingetragen 2021-11-26

\quoteon Im Kontext mit den einzigen Variablen $x : \IN$, $f : \IN \to \IN$ ist * $x$ ein Term vom Typ $\IN$, * $\lambda g\ (z:\IN). g (g\ z)$ ein Term vom Typ $(\IN \to \IN) \to \IN \to \IN$, * $f x$ ein Term vom Typ $\IN$, * $f$ ein Term von Typ $\IN \to \IN$, \quoteoff Zu einem Kontext gehören also 0 bis n Terme. Stimmt das? Ich brauche jetzt noch zu den von dir oben angegebenen 4 Termen jeweils den Kontext in der Form: Kontext $\vdash$ Term Ich versuche, dies wie folgt zu machen: (wobei ich den Kontext als Liste mit runden Klammern angebe und links des $\vdash$ die Liste und rechts davon ein Term steht. 1) ($x : \IN \:$) $\vdash$ $x : \IN$ 2) ($z: \IN, \: \lambda g.g (g\ z)):(\IN \to \IN) \to \IN \to \IN) \: $ $\vdash$ $\lambda g. g (g\ z)$ 3) ($x : \IN, \: f : \IN \to \IN \: $) $\vdash$ $fx$ 4) ($f : \IN \to \IN \:$) $\vdash$ $f$ Ist das korrekt oder wie muss das richtig gemacht werden? \quoteon Im leeren Kontext ist x überhaupt kein Term, f auch nicht. \quoteoff Welchen Sinn hat dann der leere Kontext? Kannst du mir ein einfaches Beispiel geben? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.15, eingetragen 2021-11-26

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) Es gibt nicht "den" Kontext. I.A. gibt es viele Kontexte, in denen eine Zeichenfolge (oder vielleicht etwas besser: ein "Präterm") ein Term ist. 1) Ja, $(x\colon \IN) \vdash x\colon \IN$, aber auch zum Beispiel $(x\colon \IN,f\colon \IN \to \IN) \vdash x\colon \IN$ und $(f\colon \IN,x\colon \IN \to \IN) \vdash x\colon \IN \to \IN$. 2) Ein Kontext in dem hier verwendeten Sinn ordnet lediglich Variablen Typen zu. Beliebige andere Formen von Termen stehen höchstens als Typen der Variablen drin. In Kontexten $\Gamma$, wo $\IN$ ein Typ ist, haben wir $\Gamma \vdash (\lambda g\ (z:\IN). g (g\ z)) \colon (\IN \to \IN) \to \IN \to \IN$. In dem Lambdaausdruck habe ich nur für $z$ einen Typ angegeben. Ich hätte für $g$ auch einen angeben können; der kann dann per Typinferenz aber nur $\IN \to \IN$ sein, drum habe ich das weggelassen. 3) Richtig wäre $(x\colon\IN, f\colon \IN \to \IN) \vdash f \ x\colon \IN$. 4) $(f\colon \IN \to \IN) \vdash f\colon \IN\to\IN$. Im leeren Kontext kann man auch einiges folgern. Dazu holen wir ein wenig aus. Wir haben in üblichen MLTT-Formalisierungen nicht nicht nur Urteile der Form $\Gamma \vdash t\colon \tau$, die mehr oder weniger sagen, dass im Kontext $\Gamma$ der Term $t$ den Typ $\tau$ hat, sondern auch Urteile der Form $\Gamma \vdash t\ type$, die sagen, dass der Ausdruck $t$ "ein Typ ist" -- woraus dann folgt, dass man dieses $t$ auch in $\Gamma$ erweiternden Kontexten als Typ verwenden kann. Und dann hat man zum Beispiel Regeln wie $$\begin{array}{c}\\\hline\Gamma \vdash \mathrm{Type}\ type\end{array}$$, welche sagt, dass in beliebigen Kontexten, insbesondere dem leeren, $\mathrm{Type}$ als Typ verwendet werden darf, und $$\begin{array}{c}\Gamma \vdash t \colon \mathrm{Type} \\\hline \Gamma \vdash t\ type\end{array}$$, die sagt, dass ein Ausdruck vom Typ $\mathrm{Type}$ selber auch als Typ dienen kann. Und dann gibt es etwa Regeln wie: Wenn $\Gamma$ ein Kontext ist, und $\Gamma \vdash t\ type$, dann ist auch $\Gamma, (x:t)$ ein Kontext. Wenn man das ganze vereinfacht, und einige primitive Typen durch Regeln vorgibt (das ist auch sinnvoll, aber kein gute Modellierung davon, wie Lean das tut), könnte es auch sein, dass etwa $\IN$ immer ein Typ ist, auch in einem leeren Kontext. Und dann ist $\lambda x: \IN. x$ im leeren Kontext ein Term vom Typ $\IN \to \IN$.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.16, vom Themenstarter, eingetragen 2021-11-27

I) \quoteon 2) Ein Kontext in dem hier verwendeten Sinn ordnet lediglich Variablen Typen zu. Beliebige andere Formen von Termen stehen höchstens als Typen der Variablen drin. In Kontexten $\Gamma$, wo $\IN$ ein Typ ist, haben wir $\Gamma \vdash (\lambda g\ (z:\IN). g (g\ z)) \colon (\IN \to \IN) \to \IN \to \IN$. In dem Lambdaausdruck habe ich nur für $z$ einen Typ angegeben. Ich hätte für $g$ auch einen angeben können; der kann dann per Typinferenz aber nur $\IN \to \IN$ sein, drum habe ich das weggelassen. \quoteoff Wie könnte dann ein möglicher Kontext für $(\lambda g\ (z:\IN). g (g\ z)) \colon (\IN \to \IN) \to \IN \to \IN$ aussehen? (Ich will als Anfänger trotz Typeninferenz alle Typen angeben). Mein Vorschlag: $(z:\IN \:,\: g:\IN) \vdash (\lambda g:\IN.(\lambda z:\IN. g (g\ z))):(\IN \to \IN) \to \IN \to \IN$. Ist das richtig? II) Mir ist leider noch nicht der Sinn der Angabe des Kontextes klar, denn die Variablen mit Typangabe stehen rechts vom $\vdash$ und links auch nochmals. Außer bei Beispiel 3): $(x\colon\IN, f\colon \IN \to \IN) \vdash f \ x\colon \IN$. Warum gibt man die Variablen mit Typangabe dann links vom $\vdash$ auch nochmals an? III) Regel4: $C, x : σ \quad \vdash \quad t : τ $ ------------------------------- Lam $C \quad \vdash \quad (λx : σ. t) : σ → τ $ Welchen Sinn hat dort die Angabe der Kontexte und speziell die Angabe des Kontexts x : σ ? Dieser Kontext x : σ kommt doch im Term $(λx : σ. t) : σ → τ $ nochmals vor. IV) Hätte man die Regel4 auch wie folgt modifizieren können: Regel4: $C \quad \vdash \quad t : τ $ ------------------------------- Lam $C \quad \vdash \quad (λx : σ. t) : σ → τ $ mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.17, eingetragen 2021-11-28

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) I) Nein, das ist nicht richtig. Erstens wird $g$ als Funktion benutzt, der Typ $\IN$ passt also nicht, zweitens sind in dem Term rechts vom $\vdash$ $g$ und $z$ gebunden. Es bringt also überhaupt nichts, im Kontext den Variablen $g$ und $z$ einen Typ zuzuweisen, weil es ganz andere Variablen sind. $$\Gamma \vdash (\lambda g:\IN \to \IN.(\lambda z:\IN. g (g\ z))):(\IN \to \IN) \to \IN \to \IN$$ mit beliebigen $\Gamma$ ist i.O. II) Alle freien Variablen müssen durch den Kontext zumindest einen Typ bekommen. Andernfalls kann man nicht ausrechnen, welchen Typ der Term hat. Das will man aber -- so sehr, dass "Terme" bei denen das nicht geht, gar nicht erst erlaubt sind. Und dieses "nochmal-Angeben" geschieht ja nur in den Fällen, wo der Term einfach nur 'ne Variable ist: In Kontexten mit einer Variablen $x$ vom Typ $\tau$ ist $x$ ein Term, und zwar vom Typ $\tau$. III) Variablen in Kontexten müssen eben einen Typ haben. IV) Nein. Wir wollen, dass in $t$ die Variable $x$ frei vorkommen darf. Das dürfte sie nicht, wenn sie nicht im Kontext vorkommt.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.18, vom Themenstarter, eingetragen 2021-11-28

1) Hier nochmals die 4 Regeln. Sind diese von mir richtig übersetzt ? Regel1: --------------------------------- CST wenn Konstante c den Typ σ hat $C \quad \vdash \quad c : σ $ Regel2: ------------------------------- VAR, wenn $x : σ $ das letzte Element in C ist $C \quad \vdash \quad x : σ $ Regel3: $C \quad \vdash \quad t : σ \:→ \: τ \quad$ und $\quad C \quad \vdash \quad u : σ$ ---------------------------------------------------- APP $C \quad \vdash \quad tu : τ $ Regel4: $C, x : σ \quad \vdash \quad t : τ $ ------------------------------- Lam $C \quad \vdash \quad (λx : σ. t) : σ → τ $ 2) S.8 in dem Skript wird bewiesen, dass es einen Term mit einem bestimmten Typ T (im Skript ist das ein komplexerer Typ) gibt. Genauer müsste es doch heissen, daß man zu einem vorgegebenen Typ T einen Term t mit einem Kontext K angeben (konstruieren) muss. D.h. es wurde vergessen einen Kontext zu erwähnen. Ist das richtig? 3) Prinzipiell müsste man doch zu jedem Term einen Kontext angeben, oder? Ist das richtig? 4) Als einfaches Beispiel wähle ich den Typ $\sigma \to \tau$ und versuche einen Term (mit einem Kontext) zu finden, d.h. diesen anzugeben. Dazu benutze ich die Regeln oben. Ich gehe davon aus, dass man keinen Term und keinen Kontext finden kann. Zwar gibt es zu dem Typ $\sigma \to \sigma$ einen Typ (mit Kontext), aber nicht zu dem Typ $\sigma \to \tau$ Wo ist mein Denkfehler in der Herleitung unten? Anwendung von Regel2: $(x:\sigma) \quad \vdash \quad x:\sigma$ Anwendung von Regel2: $(y:\tau) \quad \vdash \quad y:\tau$ also: $(y:\tau \: , \; x:\sigma) \quad \vdash \quad y:\tau$ Anwendung von Regel4: $(y:\tau \: , \; x:\sigma) \quad \vdash \quad y:\tau$ ------------------------------- Lam $(y:\tau) \vdash \quad (λx : σ.y:\tau) : σ → τ $ Ergebnis (vermutlich falsch): Damit gibt es zu dem Typ $\sigma \to \tau$ den Term $(λx : σ.y:\tau) : σ → τ$ und den Kontext $(y:\tau)$ mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.19, eingetragen 2021-11-29

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) 1) Sieht richtig aus. 2,3) Im Prinzip müsste man Kontexte angeben, wenn man die Regeln explizit benutzen will. Aber die Herleitung eines Terms dort auf S. 8 funktioniert in beliebigen Kontexten (zumindest solchen, wo $\alpha, \beta$ und $\gamma$ Typterme sind). 4) Ja. In Kontexten $\Gamma$ mit $\Gamma \vdash t:\tau$ hat $λx : σ. t$ den Typ $σ → τ$. Insbesondere also, mit beliebigen $\Gamma$,: $\Gamma,y:\tau \vdash (λx : σ. y): \sigma \to \tau$.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.20, vom Themenstarter, eingetragen 2021-11-29

I) Zitat S.7: --------------- Given a type σ, the type inhabitation problem consists of finding an “inhabitant” of that type—i.e., a term of type σ—within the empty local context. It may seem like a pointless exercise, but as we will see in Chapter 3, there is a close connection between this problem and the problem of finding a proof of a proposition. ---------------- a) In dem englischen Zitat oben wird ein "empty local context" vorausgesetzt. Bewiesen habe ich aber nur: $(y:\tau) \vdash (λx : σ. y): \sigma \to \tau$. für den nichtleeren lokalen Kontext $(y:\tau)$. Das obige englische Zitat angewendet, ergibt sich für mich, dass ich _nicht_ folgern kann: $\sigma \to \tau$ ist eine wahre Aussage (wird für jede Belegung wahr). Stimmt diese Argumentation? b) Anwendung von Regel2: $(x:\sigma) \quad \vdash \quad x:\sigma$ Setze in Regel4 für t den Term x und für $\tau$ den Typ $\sigma$ Anwendung von Regel4: $(x:\sigma) \quad \vdash \quad x:\sigma$ ------------------------------- Lam $() \vdash \quad (λx : σ.x:\sigma) : \sigma \to \sigma $ Also gilt für den leeren lokalen Kontext (): $\quad (λx : σ.x:\sigma) : \sigma \to \sigma $ Das englische Zitat oben angwendet ergibt: $\sigma \to \sigma $ eine wahre Aussage. Stimmt diese Argumentation? mfg cx


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.21, vom Themenstarter, eingetragen 2021-11-30

Ich will Folgendes beweisen: Es gibt einen Term mit leerem Kontext, der den Typ $\sigma \to \tau \to \sigma$ hat. Beweis: 1) Anwendung von Regel2: $(y:\tau, x:\sigma) \quad \vdash \quad x:\sigma$ 2) also: $(x:\sigma, y:\tau) \quad \vdash \quad x:\sigma$ Frage: Warum kann man das folgern ?? 3) Anwendung von Regel4: $(x:\sigma, y:\tau) \quad \vdash \quad x:\sigma$ ------------------------------------ Lam $(x:\sigma) \vdash \quad (λy : \tau.x:\sigma) : \tau \to \sigma $ 4) Anwendung von Regel4: $(x:\sigma) \vdash \quad (λy : \tau.x:\sigma) : \tau \to \sigma $ ------------------------------------ Lam $() \vdash \quad (λx : \sigma.((λy : \tau.x:\sigma) : \tau \to \sigma)) : \sigma \to \tau \to \sigma $ Also hat der folgende Term (mit leerem Kontext): $(λx : \sigma.(λy : \tau.x:\sigma) : \tau \to \sigma)$ den Typ: $\sigma \to \tau \to \sigma $ Das englische Zitat oben angwendet ergibt: $\sigma \to \tau \to \sigma$ eine wahre Aussage. Stimmt diese Argumentation?


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.22, eingetragen 2021-12-01

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) @#20 I) a) Ja. b) Ja. @#21 \quoteon Warum kann man das folgern ?? \quoteoff Man kann das zwar üblicherweise folgern, aber m.E. nicht mit ausschließlich im Skript angegebenen Regeln. Strukturelle Regeln zum Umordnen von Kontexten sind nicht erwähnt. Aber intuitiv klar sollte ja sein: Wenn $\Gamma, \Delta, x:\tau \vdash rhs$, so auch $\Gamma, x:\tau, \Delta \vdash rhs$, wenn in $\tau$ keine Variablen aus $\Delta$ verwendet werden, und $\Delta$ keine Variablen namens $x$ deklariert. Zum Rest: Ja, die Argumentation kann man so nehmen. Edit: Ergänzung: Zur Erläuterung der o.g.: Bedingungen: * Falsch: $(x: \sigma)(x: \tau) \vdash x:\sigma$; "aus Sicht des Terms" bezieht sich ein Variablenname immer auf die am weitesten rechts im Kontext stehende Variable. * Falsch: $(x : T)(T : \mathrm{Type}) \vdash x:T$; hier ist der Kontext schon gar nicht zulässig. \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.23, vom Themenstarter, eingetragen 2021-12-01

Hallo tactac, Danke für dein Feedback \quoteon Aber intuitiv klar sollte ja sein: Wenn $\Gamma, \Delta, x:\tau \vdash rhs$, so auch $\Gamma, x:\tau, \Delta \vdash rhs$, wenn in $\tau$ keine Variablen aus $\Delta$ verwendet werden, und $\Delta$ keine Variablen namens $x$ deklariert. Zum Rest: Ja, die Argumentation kann man so nehmen. Edit: Ergänzung: Zur Erläuterung der o.g.: Bedingungen: * Falsch: $(x: \sigma)(x: \tau) \vdash x:\sigma$; "aus Sicht des Terms" bezieht sich ein Variablenname immer auf die am weitesten rechts im Kontext stehende Variable. * Falsch: $(x : T)(T : \mathrm{Type}) \vdash x:T$; hier ist der Kontext schon gar nicht zulässig. \quoteoff 1) Warum ist: $(x: \sigma)(x: \tau) \vdash x:\sigma$ falsch. Dies ist deswegen falsch weil x nicht den Typ $\sigma$ und zugleich den Typ $\tau$ haben kann. (Ich verstehe deswegen deine Begründung nicht). Ist meine Begründung korrekt? 2) Dagegen ist $(x: \sigma)(y: \tau) \vdash x:\sigma$ richtig, denn es gilt doch: Wenn $\Gamma, \Delta, x:\tau \vdash rhs$, so auch $\Gamma, x:\tau, \Delta \vdash rhs$, wenn in $\tau$ keine Variablen aus $\Delta$ verwendet werden, und $\Delta$ keine Variablen namens $x$ deklariert. Setze: $\Gamma$ := () $\Delta := y:\tau$ $rhs := x:\sigma$ Ist meine Begründung korrekt? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.24, eingetragen 2021-12-01

1) Naja, man kann sog. „Shadowing“ zulassen. Dann kann es mehrere Variablen gleichen Namens geben. So ist es auch in dem Beispiel: wir haben zwei Variablen names „x“ im Kontext. Welche gemeint ist, wenn im Term ein Variablenname auftaucht, wird dann eben so geregelt, dass das immer die „nächstliegende“ ist (falls überhaupt eine mit dem Namen vorhanden ist). 2) Ja.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.25, vom Themenstarter, eingetragen 2021-12-02

Hallo Tactac, vielen Dank für dein Feedback. Jetzt ist mir schon Einiges klarer. I) \quoteon Man kann das zwar üblicherweise folgern, aber m.E. nicht mit ausschließlich im Skript angegebenen Regeln. Strukturelle Regeln zum Umordnen von Kontexten sind nicht erwähnt. Aber intuitiv klar sollte ja sein: Wenn $\Gamma, \Delta, x:\tau \vdash rhs$, so auch $\Gamma, x:\tau, \Delta \vdash rhs$, wenn in $\tau$ keine Variablen aus $\Delta$ verwendet werden, und $\Delta$ keine Variablen namens $x$ deklariert. \quoteoff a) "Strukturelle Regeln zum Umordnen von Kontexten sind nicht erwähnt". Dann sind die Regeln nicht vollständig und ich kann - die Infos des Skripts verwendend - nicht ausreichend argumentieren. Ist das richtig? b) Deswegen wende ich mich an das von dir mehrfach erwähnte HoTT-Buch. Kannst du mir das - Exaktheit der Dartellung betreffend - empfehlen ? c) Habe die "Strukturelle Regeln zum Umordnen von Kontexten" im HoTT nicht gefunden bzw. wo kommen diese vor? https://hott.github.io/book/nightly/hott-online-1287-g1ac9408.pdf Auf Seite 432 dieses HoTT-Buches Kapitel A.2.1 Contexts: https://hott.github.io/book/nightly/hott-online-1287-g1ac9408.pdf wird Contexts definiert. Ich habe da Problem, dass in Regel 2 einmal der Kontext eine Liste ohne runde Klammern ist und das andere Mal mit Klammern. Kannst du mir das erklären? II) \quoteon Wir haben in üblichen MLTT-Formalisierungen nicht nicht nur Urteile der Form $\Gamma \vdash t\colon \tau$, die mehr oder weniger sagen, dass im Kontext $\Gamma$ der Term $t$ den Typ $\tau$ hat, sondern auch Urteile der Form $\Gamma \vdash t\ type$, die sagen, dass der Ausdruck $t$ "ein Typ ist" -- woraus dann folgt, dass man dieses $t$ auch in $\Gamma$ erweiternden Kontexten als Typ verwenden kann. Und dann hat man zum Beispiel Regeln wie $$\begin{array}{c}\\\hline\Gamma \vdash \mathrm{Type}\ type\end{array}$$, welche sagt, dass in beliebigen Kontexten, insbesondere dem leeren, $\mathrm{Type}$ als Typ verwendet werden darf, und $$\begin{array}{c}\Gamma \vdash t \colon \mathrm{Type} \\\hline \Gamma \vdash t\ type\end{array}$$, die sagt, dass ein Ausdruck vom Typ $\mathrm{Type}$ selber auch als Typ dienen kann. Und dann gibt es etwa Regeln wie: Wenn $\Gamma$ ein Kontext ist, und $\Gamma \vdash t\ type$, dann ist auch $\Gamma, (x:t)$ ein Kontext. \quoteoff a) was ist type? Ein reserviertes Wort oder ist dies ein von dir frei gewählter Namen, den man hätte auch anders wählen können? Für was steht das type? Type ist doch ein reserviertes Wort, warum braucht man dann noch type? b) Habe dazu im HoTT-Buch nichts gefunden, bzw. übersehen. Wo steht das ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.26, eingetragen 2021-12-04

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) I) a) Ja, vielleicht. Andererseits habe ich aber nochmal gelesen, was die da genau schreiben. $$\begin{array}{c}\\\hline C \vdash x \colon \sigma\end{array} \mathsf{Var}\text{ if $x : σ$ is the last occurrence of $x$ in C}$$ Den Teil "of x" hatte ich bis jetzt nicht gebührend zur Kenntnis genommen. Es bewirkt aber: Korrektes Shadowing ist da mit drin, und Kontext-Umordnung nicht erforderlich. Es ist eben so, wie man es intuitiv haben wollen würde. b) Ja, kann ich empfehlen. Darüberhinaus: Mario Carneiros "The Type Theory of Lean" (https://github.com/digama0/lean-type-theory/releases) ist aber auch nicht verkehrt. c) Kommen nicht vor. Sie sind eh nicht ausreichend, und es gibt bessere Alternativen. Was du mit "Regel 2" meinst, ist mir nicht ersichtlich. Zitiere bei Ortsangaben doch ein wenig Text drumherum. II) a) Ich spreche dort von gänzlich verschiedenen Urteilsformen. Man kann in dem Sinn "type" zwar als reserviertes Wort ansehen. Aber das ist eher Metasyntax. Es ist jedenfalls nicht so, dass durch geeignete Substitution $\Gamma \vdash t:T$ dasselbe wird wie $\Gamma \vdash U\ {type}$. Allenfalls durch Schlussregeln kann man die in Beziehung setzen. b) im HoTT-Buch steht das wichtigste m.E. auch. Davon ab: Die verschiedenen Urteilsformen findet man immer mal in diversen Papers in https://arxiv.org/list/cs.LO/recent \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.27, vom Themenstarter, eingetragen 2021-12-04

\quoteon(2021-12-04 01:26 - tactac in Beitrag No. 26) \quoteon I) a) Ja, vielleicht. Andererseits habe ich aber nochmal gelesen, was die da genau schreiben. $$\begin{array}{c}\\\hline C \vdash x \colon \sigma\end{array} \mathsf{Var}\text{ if $x : σ$ is the last occurrence of $x$ in C}$$ Den Teil "of x" hatte ich bis jetzt nicht gebührend zur Kenntnis genommen. Es bewirkt aber: Korrektes Shadowing ist da mit drin, und Kontext-Umordnung nicht erforderlich. \quoteoff Warum ist dazu Kontext-Umordnung nicht erforderlich? Kannst du das an meinem Beispiel zeigen, wie du da ohne auskommst? \quoteon c) Kommen nicht vor. Sie sind eh nicht ausreichend, und es gibt bessere Alternativen. \quoteoff Kannst du mir eine Quelle nennen, wo die Regeln ausreichend sind und die ich deiner Meinung nach benutzen soll? \quoteon Was du mit "Regel 2" meinst, ist mir nicht ersichtlich. Zitiere bei Ortsangaben doch ein wenig Text drumherum. \quoteoff ------ ctx-EMP (Regel1) ·ctx $x_1:A_1, . . . , x_{n−1} : A_{n−1} \vdash A_n : U_i$ ------------------------------------------- ctx-EXT (Regel2) $(x_1 :A_1, . . . , x_n : A_n ) \: ctx $ \quoteon II) a) Ich spreche dort von gänzlich verschiedenen Urteilsformen. Man kann in dem Sinn "type" zwar als reserviertes Wort ansehen. Aber das ist eher Metasyntax. Es ist jedenfalls nicht so, dass durch geeignete Substitution $\Gamma \vdash t:T$ dasselbe wird wie $\Gamma \vdash U\ {type}$. Allenfalls durch Schlussregeln kann man die in Beziehung setzen. \quoteoff ... "type" zwar als reserviertes Wort ... wie siehst du das bzw. wie verwendest du das ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.28, eingetragen 2021-12-05

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-12-04 10:34 - carlox in Beitrag No. 27) \quoteon(2021-12-04 01:26 - tactac in Beitrag No. 26) \quoteon I) a) Ja, vielleicht. Andererseits habe ich aber nochmal gelesen, was die da genau schreiben. $$\begin{array}{c}\\\hline C \vdash x \colon \sigma\end{array} \mathsf{Var}\text{ if $x : σ$ is the last occurrence of $x$ in C}$$ Den Teil "of x" hatte ich bis jetzt nicht gebührend zur Kenntnis genommen. Es bewirkt aber: Korrektes Shadowing ist da mit drin, und Kontext-Umordnung nicht erforderlich. \quoteoff Warum ist dazu Kontext-Umordnung nicht erforderlich? Kannst du das an meinem Beispiel zeigen, wie du da ohne auskommst? \quoteoff\quoteoff Wie ich die Regelbeschreibung nun verstehe, hat man eben einfach $\begin{array}{c} \\\hline (x:T)(y:T) \vdash x:T\end{array}$ und $\begin{array}{c} \\\hline (x:T)(x:S)(y:T) \vdash x:S\end{array}$, aber $\begin{array}{c} \\\hline (x:T)(x:S)(y:T) \vdash x:T\end{array}$ nicht. \quoteon \quoteon c) Kommen nicht vor. Sie sind eh nicht ausreichend, und es gibt bessere Alternativen. \quoteoff Kannst du mir eine Quelle nennen, wo die Regeln ausreichend sind und die ich deiner Meinung nach benutzen soll? \quoteoff Carneiro sollte auf jeden Fall reichen. \quoteon\quoteon Was du mit "Regel 2" meinst, ist mir nicht ersichtlich. Zitiere bei Ortsangaben doch ein wenig Text drumherum. \quoteoff ------ ctx-EMP (Regel1) ·ctx $x_1:A_1, . . . , x_{n−1} : A_{n−1} \vdash A_n : U_i$ ------------------------------------------- ctx-EXT (Regel2) $(x_1 :A_1, . . . , x_n : A_n ) \: ctx $ \quoteon \quoteoff\quoteoff Ok. Da geht es um Kontexterweiterungen. Und es sagt etwa das aus, was ich in #15 schrieb, ohne einen Umweg über ein Urteil der Form $\Gamma \vdash bla \ type$. Die runden Klammern sind nicht so wichtig, "bla ist ein Kontext" wird da eben so geschrieben, mehr ist da nicht dran. \quoteon\quoteon II) a) Ich spreche dort von gänzlich verschiedenen Urteilsformen. Man kann in dem Sinn "type" zwar als reserviertes Wort ansehen. Aber das ist eher Metasyntax. Es ist jedenfalls nicht so, dass durch geeignete Substitution $\Gamma \vdash t:T$ dasselbe wird wie $\Gamma \vdash U\ {type}$. Allenfalls durch Schlussregeln kann man die in Beziehung setzen. \quoteoff ... "type" zwar als reserviertes Wort ... wie siehst du das bzw. wie verwendest du das ? \quoteoff\quoteoff Ich habe da keine gefestigte Meinung im Sinne von "Ja, genau so sollte man es hinschreiben, dann ist alles total super und klar". \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1371
  Beitrag No.29, vom Themenstarter, eingetragen 2021-12-05

\quoteon Wie ich die Regelbeschreibung nun verstehe, hat man eben einfach $\begin{array}{c} \\\hline (x:T)(y:T) \vdash x:T\end{array}$ und $\begin{array}{c} \\\hline (x:T)(x:S)(y:T) \vdash x:S\end{array}$, aber $\begin{array}{c} \\\hline (x:T)(x:S)(y:T) \vdash x:T\end{array}$ nicht. \quoteoff Das verstehe ich nicht. "if x:σ is the last occurrence of x in C" bedeutet doch, dass x ganz links (letztes Vorkommen) im Kontext vorkommen muss. Und das macht es doch bei deinen 3 Beispielen: x:T \quoteon ------ ctx-EMP (Regel1) ·ctx $x_1:A_1, . . . , x_{n−1} : A_{n−1} \vdash A_n : U_i$ ------------------------------------------- ctx-EXT (Regel2) $(x_1 :A_1, . . . , x_n : A_n ) \: ctx $ Ok. Da geht es um Kontexterweiterungen. Und es sagt etwa das aus, was ich in #15 schrieb, ohne einen Umweg über ein Urteil der Form $\Gamma \vdash bla \ type$. Die runden Klammern sind nicht so wichtig, "bla ist ein Kontext" wird da eben so geschrieben, mehr ist da nicht dran. \quoteoff Was bedeutet bei Regel1 das ctx? (das wird nirgends definiert) Kannst du mir ein einfaches Beispiel dazu geben ? Was bedeutet bei Regel2 das ctx? (das wird nirgends definiert) Kannst du mir ein einfaches Beispiel dazu geben ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2332
  Beitrag No.30, eingetragen 2022-01-01 04:24

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-12-05 12:21 - carlox in Beitrag No. 29) \quoteon Wie ich die Regelbeschreibung nun verstehe, hat man eben einfach $\begin{array}{c} \\\hline (x:T)(y:T) \vdash x:T\end{array}$ und $\begin{array}{c} \\\hline (x:T)(x:S)(y:T) \vdash x:S\end{array}$, aber $\begin{array}{c} \\\hline (x:T)(x:S)(y:T) \vdash x:T\end{array}$ nicht. \quoteoff Das verstehe ich nicht. "if x:σ is the last occurrence of x in C" bedeutet doch, dass x ganz links (letztes Vorkommen) im Kontext vorkommen muss. Und das macht es doch bei deinen 3 Beispielen: x:T \quoteoff "the last occurence" ist die rechteste. \quoteon \quoteon ------ ctx-EMP (Regel1) ·ctx $x_1:A_1, . . . , x_{n−1} : A_{n−1} \vdash A_n : U_i$ ------------------------------------------- ctx-EXT (Regel2) $(x_1 :A_1, . . . , x_n : A_n ) \: ctx $ Ok. Da geht es um Kontexterweiterungen. Und es sagt etwa das aus, was ich in #15 schrieb, ohne einen Umweg über ein Urteil der Form $\Gamma \vdash bla \ type$. Die runden Klammern sind nicht so wichtig, "bla ist ein Kontext" wird da eben so geschrieben, mehr ist da nicht dran. \quoteoff Was bedeutet bei Regel1 das ctx? (das wird nirgends definiert) Kannst du mir ein einfaches Beispiel dazu geben ? Was bedeutet bei Regel2 das ctx? (das wird nirgends definiert) Kannst du mir ein einfaches Beispiel dazu geben ? mfg cx \quoteoff Das "ctx" bedeutet einfach nur "ist ein zulässiger Kontext". Es geht da um die Frage, welche Möglichkeiten es gibt, neue Kontexte aus alten zu bauen. Und aufs wesentliche reduziert sagt die Regel: wenn $A$ im Kontext $\Gamma$ ein Typ ist, ist $\Gamma, x:A$ ein weiterer zulässiger Kontext. Einfaches Beispiel: Man kann es so basteln, dass z.B. $\IN$ in jedem Kontext ein Typ ist. Dann wäre der Kontext, der nur eine Variable namens $x$ vom Typ $\IN$ enthält, ein zulässiger Kontext.\(\endgroup\)


   Profil
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.

Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2022 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]