Структура и теоремы

Путешествует хоть логика.

Посмотри на это.

    void greet() {
	String hello = getHello();
	String subject = getSubject(1);
	showGreeting(hello, subject);
    }

    private String getHello() {
	return "Hello";
    }

    private String getSubject(int i) {
	if (i == 0) {
	    return "Fred";
	}
	if (i == 1) {
	    return "world";
	}
	return "everybody";
    }

    private void showGreeting(String hail, String subject) {
	System.out.println(hail + ", " + subject + ".");
    }

Утомительный, смехотворно перегруженный Java-код, но разве это теорема?

Суд по терминологии.

Первый: что такое теорема?

Хорошо, старая вики говорит нам, что «Логика … рассматривает теоремы как утверждения (называемые формулами или правильно сформированными формулами) формального языка. Должен быть предоставлен набор правил вывода, также называемых правилами преобразования или правилами вывода. Эти правила вывода точно указывают, когда формула может быть получена из набора предпосылок «. И далее: «Первоначально принятые формулы в выводе называются его аксиомами и являются основой, на которой основывается теорема».

То, что «… получено из ряда предпосылок», подразумевает, что теоремы могут быть доказаны там, где, опять же, вики «доказательство является дедуктивным аргументом для математического утверждения», и далее « Дедуктивное рассуждение связывает предпосылки с выводами. все предпосылки верны, условия понятны, и правила дедуктивной логики соблюдаются, тогда сделанный вывод обязательно верен ».

Что же это за любопытный зверь, дедуктивное мышление?

Дедуктивное мышление.

При первом изучении дедукции студенты обычно сталкиваются с силлогизмом, в котором утверждение следует из двух других:

1. Все люди смертны.
2. Аристотель — мужчина.
3. Следовательно, Аристотель смертен.

Этот силлогизм — « Смертный Аристотель », силлогизм — имеет две предпосылки: первое, что все люди смертны, и второе, что Аристотель — человек. Затем он предлагает сделать вывод из этих предпосылок, а именно, что Аристотель смертен. Принимая во внимание то, что большинство считает, что «все люди смертны» и «Аристотель — человек» в качестве изначально принятых утверждений (или, на языке определения Вики, формул), а также учитывая, что Мортал Аристотель использует вычет для производства В заключение, силлогизм, по-видимому, отвечает всем критериям теоремы. Правда, это может быть просто частичка теоремы, гомеопатическая настойка теоремы, но, тем не менее, теорема такова.

Здесь исследование того, может ли исходный код быть теоремой, может выиграть от временной инверсии: может ли эта теорема Мортал Аристотель быть записана как исходный код? И конечно может.

    class Aristotle extends Man {
       .
       .
       .
    }

    boolean isMortal(Object object) {
	return object instanceof Man;
    }
    System.out.println(isMortal(new Aristotle()));

Этот код, безусловно, выглядит со стороны. У него есть Человек, Аристотель и даже что-то вроде вычета смертности. Это безобразие instanceofне должно отвлекать ученика от того, как метод воплощает дедукцию, выводя свойства вещей из свойств других вещей. Форма, которую принимает код — тонкости вывода свойств — вряд ли имеет значение; любое количество альтернатив тоже подойдет. Например:

    boolean isMortal(Creature creature) {
	return creature.hasProperty(Property.Man);
    }

Или метод в предлагаемом Manклассе:

    @Override
    boolean isMortal() {
	return hasProperty(Property.MORTAL);
    }

Или даже:

    @Override
    boolean isMortal() {
	return true;
    }

Основной вычет остается.

Но помимо демонстрации определенного произвола реализации, эти примеры не могут кристаллизовать основной вывод. Какое устройство могло бы придумать человечество, чтобы сделать резкий вывод из такой белой мраморной предпосылки?

Ответ: человечество в глубине древности создало устройство редкой ценности. Это устройство дает нам основание рационального мышления, непоколебимо глубокое, звучно названное «Modus ponens».

Модус поненс.

Modus ponens , одно из немногих формальных правил дедукции, позволяет делать выводы из других утверждений. Он достаточно силен, чтобы взвесить всю систему логики на широкие плечи, и находит выражение в форме:

1. Утверждение P подразумевает утверждение Q.
2. Утверждение P верно.
3. Следовательно, утверждение Q верно.

Эти несколько строк раскрывают сущность дедуктивной логики: первая предпосылка — условная — объединяется со второй предпосылкой, чтобы логически вывести заключение. Более того, условная предпосылка разлагается на антецедент P и последующее Q. Во второй предпосылке просто утверждается P, антецедент условного, в то время как заключение выводит истинность Q, как условного следствия.

Обе предпосылки могут быть как истинными, так и ложными, если modus ponens гарантирует сохранение правды. Если оба предположения верны, то заключение должно быть верным. Таким ревом Модус Поненс.

В удивительно краткой символике логики, где → обозначает логическое значение, а ∴ обозначает «поэтому», modus ponens использует следующую приятную стенографию.

P → Q, P ∴ Q

Это читается как: «Учитывая, что P подразумевает, что Q истинно, а учитывая, что P истинно, следовательно, Q должно быть истинно».

(Логика, как правило, опускает «истинно», соглашаясь на: «Учитывая P подразумевает Q и данный P, поэтому Q.». Программисты отмечают здесь свою собственную историю, обычно интерпретируя условное выражение как: ifP thenQ.)

Смертный Аристотель, таким образом, проявляет себя как просто modus ponens в симпатичном парике, и, учитывая, что, как мы видели выше, Mortal Aristotle является одной из простейших форм теоремы, поэтому каждый modus ponens тоже носит тег «Теорема», имя , Так можем ли мы извлечь из Смертного Аристотеля три определяющих элемента modus ponens? Ответ на этот вопрос приводит нас к основному утверждению: программный метод выражает условную предпосылку modus ponens.

    class Aristotle extends Man {
       .
       .
       .
    }

    boolean isMortal(Object object) {
	return object instanceof Man;
    }
    System.out.println(isMortal(new Aristotle()));

В этом случае условная предпосылка гласит: объект, являющийся экземпляром класса Man, подразумевает его смертность. Или в более дружественной для программиста формеif-then : если объект является экземпляром Manкласса, тогда этот объект смертелен . Фактический механизм реализации этого условия включает семантику имени метода и каждого последнего фрагмента его аргументов, тела и возвращаемого значения.

Сама структура класса охватывает вторую предпосылку, хотя, как видно выше, такая специфика не ограничивает общности. В Aristotleпроисходящем классе из Manкласса , таким образом , утверждает: объект является экземпляром класса Man .Aristotle

    private String getHello() {
	return "Hello";
    }

    private String getSubject(int i) {
	if (i == 0) {
	    return "Fred";
	}
	if (i == 1) {
	    return "world";
	}
	return "everybody";
    }

    private void showGreeting(String hail, String subject) {
	System.out.println(hail + ", " + subject + ".");
    }

    void greet() {
	String hello = getHello();
	String subject = getSubject(1);
	showGreeting(hello, subject);
    }

    /**  This method may return null if the field does not exist.*/
    public static Terms getTerms(IndexReader r, String field) 
	throws IOException {
	final Fields fields = getFields(r);
	if (fields == null) {
	    return null;
	} else {
	    return fields.terms(field);
	}
    }